`Compfiles/Bulgaria1998P6.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

5 declarations, 0 contain sorry, 0 declared as axioms

Bulgarian Mathematical Olympiad 1998, Problem 6

Prove that the equation

x²y² = z²(z² - x² - y²)

has no solutions in positive integers.

Imports (5)

Imported by 1 file

Compfiles.lean

lemma Bulgaria1998P6.sq_mod_four_of_odd The square of an odd integer is 1 modulo 4 line 35 source
Source documentation
The square of an odd integer is 1 modulo 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, HMod.hMod, OfNat.ofNat, HPow.hPow, Nat
Proof uses: HAdd.hAdd, HMul.hMul, Odd, Iff.mpr, Int.odd_iff, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul and 27 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma sq_mod_four_of_odd {z : ℤ} (hz : z % 2 = 1) : z ^ 2 % 4 = 1 := by
…
```
lemma Bulgaria1998P6.descent_aux Documented declaration: descent_aux line 43 source
Source documentation
The descent step for the case where the even leg is a square: from coprime p, q of opposite parity with a = p ^ 2 + q ^ 2 and b ^ 2 = 4 * p * q * (p ^ 2 - q ^ 2) we produce a smaller solution of A ^ 4 = B ^ 4 + C ^ 2 in positive naturals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LT.lt, OfNat.ofNat, Eq, Nat, Int.gcd, Or, And, HMod.hMod, HAdd.hAdd, HPow.hPow, HMul.hMul, HSub.hSub, Dvd.dvd, Exists, Int.natAbs
Proof uses: Iff.mp, mul_right_inj', Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.add_eq_eq, Eq.symm, Mathlib.Tactic.LinearCombination.mul_const_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr and 112 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 186 steps
Open to load the checked before-and-after goal states.
```
lemma descent_aux {a b p q : ℤ} (ha : 0 < a) (_hb : 0 < b)
    (hp : 0 < p) (hq : 0 < q) (hpq : q < p)
    (hgcd : Int.gcd p q = 1)
    (hpar : (p % 2 = 0 ∧ q % 2 = 1) ∨ (p % 2 = 1 ∧ q % 2 = 0))
    (haeq : a = p ^ 2 + q ^ 2)
    (hbeq : b ^ 2 = 4 * (p * q * (p ^ 2 - q ^ 2)))
    (hb2 : 2 ∣ b) :
    ∃ A B C : ℕ, 0 < A ∧ 0 < B ∧ 0 < C ∧ A < Int.natAbs a ∧ A ^ 4 = B ^ 4 + C ^ 2 := by
…
```
lemma Bulgaria1998P6.lemma_1' line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HPow.hPow, HAdd.hAdd, False
Proof uses: Nat.strongRecOn, Int, cast, Eq.symm, Eq.trans, congr, congrArg, dite, Nat.gcd, Nat.Coprime, Decidable.byContradiction, Not, And, Nat.Prime, Dvd.dvd, Exists, Iff.mp, Nat.Prime.not_coprime_iff_dvd, dvd_trans, pow_dvd_pow and 161 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 221 steps (first 200 of 221)
Open to load the checked before-and-after goal states.
lemma Bulgaria1998P6.lemma_1 line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LT.lt, OfNat.ofNat, Eq, HSub.hSub, HPow.hPow, Nat, False
Proof uses: HAdd.hAdd, eq_add_of_sub_eq', Exists, CanLift.prf, LE.le, Int.le_of_lt, Iff.mp, Int.natCast_pos, Int.ofNat_inj, Bulgaria1998P6.lemma_1'
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
problem Bulgaria1998P6.bulgaria1998_p6 line 409 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HPow.hPow, Nat, HSub.hSub, False
Proof uses: HAdd.hAdd, Neg.neg, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 121 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.