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

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1974, Problem 3

Prove that the sum from k = 0 to n inclusive of Choose[2n + 1, 2k + 1] * 2³ᵏ is not divisible by 5 for any integer n ≥ 0.

Imports (3)

Imported by 1 file

Compfiles.lean

lemma Imo1974P3.sum_range_two_mul line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Eq, Finset.sum, Finset.range, HMul.hMul, OfNat.ofNat, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, Finset, MulZeroClass.mul_zero, eq_self, Eq.mpr, id, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.add_congr and 19 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo1974P3.im_sum line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Zsqrtd, OfNat.ofNat, Int, Eq, Zsqrtd.im, Finset.sum
Proof uses: Finset.cons_induction, Eq.refl, EmptyCollection.emptyCollection, Not, Membership.mem, Eq.mpr, Finset.cons, HAdd.hAdd, id, congrArg, Finset.sum_cons, Zsqrtd.im_add
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1974P3.sqrtd_pow_two_mul line 54 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Zsqrtd, OfNat.ofNat, Int, HPow.hPow, Zsqrtd.sqrtd, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, MulZeroClass.mul_zero, pow_zero, Int.cast_one, eq_self, Eq.mpr, HAdd.hAdd, id, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.add_congr and 32 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo1974P3.im_pow The binomial sum is the coefficient of √8 in (√8 + 1)^(2n+1) line 65 source
Source documentation
The binomial sum is the coefficient of √8 in (√8 + 1)^(2n+1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Zsqrtd.im, OfNat.ofNat, HPow.hPow, Zsqrtd, HAdd.hAdd, Zsqrtd.sqrtd, HMul.hMul, Finset.sum, Finset.range, Nat.choose
Proof uses: Eq.mpr, HSub.hSub, id, congrArg, add_pow, Imo1974P3.im_sum, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, 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.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 34 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma im_pow (n : ℕ) :
    ((Zsqrtd.sqrtd + 1 : ℤ√8) ^ (2 * n + 1)).im =
      ∑ k ∈ range (n + 1), ((2 * n + 1).choose (2 * k + 1) : ℤ) * 8 ^ k := by
…
```
lemma Imo1974P3.norm_pow line 77 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Zsqrtd.norm, OfNat.ofNat, HPow.hPow, Zsqrtd, HAdd.hAdd, Zsqrtd.sqrtd, Neg.neg
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, congr, HSub.hSub, HMul.hMul, Zsqrtd.re, Zsqrtd.im, zero_add, mul_one, add_zero, eq_self, eq_true, True.intro, Trans.trans, MonoidHom, Zsqrtd.normMonoidHom, rfl and 4 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
problem Imo1974P3.imo1974_p3 line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, Finset.sum, Finset.range, HAdd.hAdd, HMul.hMul, Nat.choose, HPow.hPow
Proof uses: Eq, rfl, Int, Zsqrtd.im, Zsqrtd, Zsqrtd.sqrtd, Eq.mpr, id, congrArg, Imo1974P3.im_pow, Eq.trans, Nat.cast_sum, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Nat.cast_mul, Nat.cast_pow, pow_mul, of_eq_true and 42 more
101 instances, coercions and auxiliary constants left out.

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