`Compfiles/Imo1981P3.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

19 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1981, Problem 3

Determine the maximum value of m ^ 2 + n ^ 2, where m and n are integers in {1, 2, ..., 1981} and (n ^ 2 - m * n - m ^ 2) ^ 2 = 1.

Imports (5)

Imported by 1 file

Compfiles.lean

structure Imo1981P3.ProblemPredicate N = 1981 line 41 source
Source comment
N = 1981

standard axioms: propext what this means
Statement uses: Nat, Int
```
structure ProblemPredicate (m n : ℤ) : Prop where
…
```
def Imo1981P3.specifiedSet line 46 source
standard axioms: propext what this means
Statement uses: Nat, Set, Int
Proof uses: Set.ofPred, Exists, And, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Imo1981P3.ProblemPredicate
7 instances, coercions and auxiliary constants left out.
theorem Imo1981P3.ProblemPredicate.m_le_n line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Imo1981P3.ProblemPredicate, LE.le
Proof uses: Decidable.byContradiction, Not, Eq, OfNat.ofNat, HPow.hPow, HSub.hSub, HMul.hMul, Mathlib.Tactic.LinearCombination.eq_of_eq, HAdd.hAdd, Eq.symm, Imo1981P3.ProblemPredicate.eq_one, 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 79 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo1981P3.ProblemPredicate.eq_imp_1 line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Imo1981P3.ProblemPredicate, Eq, OfNat.ofNat
Proof uses: HMul.hMul, Mathlib.Tactic.LinearCombination.eq_of_eq, HPow.hPow, HSub.hSub, HAdd.hAdd, Imo1981P3.ProblemPredicate.eq_one, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul and 52 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo1981P3.ProblemPredicate.reduction line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Imo1981P3.ProblemPredicate, LT.lt, OfNat.ofNat, HSub.hSub
Proof uses: Eq, Or, LE.le.eq_or_lt, Imo1981P3.ProblemPredicate.m_le_n, Imo1981P3.ProblemPredicate.eq_imp_1, absurd, Eq.symm, LT.lt.ne, Imo1981P3.ProblemPredicate.mk, Iff.mpr, sub_pos, HAdd.hAdd, Trans.trans, LE.le, sub_lt_self, And.left, Imo1981P3.ProblemPredicate.m_range, And.right, Imo1981P3.ProblemPredicate.n_range, And.intro and 69 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo1981P3.NatPredicate It will be convenient to have the lemmas above in their natural number form line 98 source
Source comment
It will be convenient to have the lemmas above in their natural number form. Most of these can be proved with the `norm_cast` family of tactics.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: Imo1981P3.ProblemPredicate, Int
2 instances, coercions and auxiliary constants left out.
```
def NatPredicate (m n : ℕ) : Prop :=
…
```
theorem Imo1981P3.NatPredicate.m_le_n line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1981P3.NatPredicate, LE.le
Proof uses: cast, Int, Imo1981P3.ProblemPredicate.m_le_n
15 instances, coercions and auxiliary constants left out.
theorem Imo1981P3.NatPredicate.eq_imp_1 line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1981P3.NatPredicate, Eq, OfNat.ofNat
Proof uses: cast, Int, Eq.trans, congrArg, Eq.symm, Nat.cast_one, Imo1981P3.ProblemPredicate.eq_imp_1
13 instances, coercions and auxiliary constants left out.
theorem Imo1981P3.NatPredicate.reduction line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1981P3.NatPredicate, LT.lt, OfNat.ofNat, HSub.hSub
Proof uses: LE.le, Imo1981P3.NatPredicate.m_le_n, cast, Imo1981P3.ProblemPredicate, Int, congrFun', congrArg, Imo1981P3.ProblemPredicate.reduction, Eq.symm, Eq.trans, Nat.cast_one
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo1981P3.NatPredicate.n_pos line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1981P3.NatPredicate, LT.lt, OfNat.ofNat
Proof uses: cast, Int, Eq.trans, congrFun', congrArg, Eq.symm, Nat.cast_zero, And.left, LE.le, Imo1981P3.ProblemPredicate.n_range
24 instances, coercions and auxiliary constants left out.
theorem Imo1981P3.NatPredicate.m_pos line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1981P3.NatPredicate, LT.lt, OfNat.ofNat
Proof uses: cast, Int, Eq.trans, congrFun', congrArg, Eq.symm, Nat.cast_zero, And.left, LE.le, Imo1981P3.ProblemPredicate.m_range
24 instances, coercions and auxiliary constants left out.
theorem Imo1981P3.NatPredicate.n_le_N line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1981P3.NatPredicate, LE.le
Proof uses: cast, Int, And.right, LT.lt, OfNat.ofNat, Imo1981P3.ProblemPredicate.n_range
18 instances, coercions and auxiliary constants left out.
theorem Imo1981P3.NatPredicate.imp_fib Now we can use induction to show that solutions must be Fibonacci numbers line 123 source
Source comment
Now we can use induction to show that solutions must be Fibonacci numbers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1981P3.NatPredicate, Exists, And, Eq, Nat.fib, HAdd.hAdd, OfNat.ofNat
Proof uses: Nat.strong_induction_on, LT.lt, LE.le, Imo1981P3.NatPredicate.m_le_n, Nat.succ, Or, LE.le.eq_or_lt, Iff.mpr, Nat.succ_le_iff, Imo1981P3.NatPredicate.n_pos, Exists.intro, Imo1981P3.NatPredicate.m_pos, Eq.mpr, id, Eq.trans, True, congrArg, of_decide_eq_true, Bool, Decidable.decide and 15 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem imp_fib {n : ℕ} : ∀ m : ℕ, NatPredicate N m n → ∃ k : ℕ, m = fib k ∧ n = fib (k + 1) := by
…
```
Mentions: Imo1981P3.NatPredicate
theorem Imo1981P3.m_n_bounds line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, Nat.fib, OfNat.ofNat, Imo1981P3.NatPredicate, And, LE.le
Proof uses: Eq, Exists, Imo1981P3.NatPredicate.imp_fib, dite, Iff.mp, Nat.succ, Nat.lt_succ_iff, And.intro, Trans.trans, Nat.fib_mono, Nat.succ_le_succ, Not, not_lt, Eq.mp, congrArg, Eq.symm, Nat.fib_add_two, Imo1981P3.NatPredicate.n_le_N, absurd, LE.le.not_gt
22 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
theorem Imo1981P3.k_bound line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, Nat.fib, OfNat.ofNat, Eq, HPow.hPow, Int, Imo1981P3.ProblemPredicate, LE.le
Proof uses: LT.lt.le, And.left, Imo1981P3.ProblemPredicate.m_range, Imo1981P3.ProblemPredicate.n_range, Int.natAbs, And, Imo1981P3.m_n_bounds, Eq.mp, congrArg, Eq.symm, Int.natAbs_of_nonneg, Iff.mp, Int.natAbs_le_iff_sq_le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 61 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo1981P3.solution_bound line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, Nat.fib, OfNat.ofNat, Eq, HPow.hPow, Int, Membership.mem, Set, Imo1981P3.specifiedSet, LE.le
Proof uses: Imo1981P3.ProblemPredicate, Imo1981P3.k_bound
25 instances, coercions and auxiliary constants left out.
theorem Imo1981P3.solution_greatest line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, Nat.fib, OfNat.ofNat, Eq, HPow.hPow, Imo1981P3.ProblemPredicate, Int, IsGreatest, Imo1981P3.specifiedSet
Proof uses: And.intro, Membership.mem, Set, upperBounds, Exists.intro, Exists, And, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.cast_add, congr, Nat.cast_pow, eq_self, Imo1981P3.solution_bound
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
determine Imo1981P3.solution line 200 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo1981P3.imo1981_p3 line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsGreatest, Int, Imo1981P3.specifiedSet, OfNat.ofNat, Nat, Imo1981P3.solution
Proof uses: LT.lt, HAdd.hAdd, Nat.fib, Eq, HPow.hPow, Imo1981P3.ProblemPredicate, Imo1981P3.solution_greatest, Eq.mp, implies_congr, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, congr, congrFun', Mathlib.Meta.NormNum.isNat_natCast, of_decide_eq_true, id, Bool and 18 more
76 instances, coercions and auxiliary constants left out.

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