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

16 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2004, Problem 6

We call a positive integer alternating if every two consecutive digits in its decimal representation are of different parity.

Find all positive integers n such that n has a multiple that is alternating.

Imports (2)

Imported by 1 file

Compfiles.lean

determine Imo2004P6.SolutionSet line 28 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Not, Dvd.dvd
3 instances, coercions and auxiliary constants left out.
abbrev Imo2004P6.Alternating line 30 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, LT.lt, OfNat.ofNat, List.IsChain, Not, Nat.ModEq, Nat.digits
2 instances, coercions and auxiliary constants left out.
lemma Imo2004P6.not_alternating_of_dvd_twenty line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, OfNat.ofNat, Not, Imo2004P6.Alternating
Proof uses: LT.lt, List.IsChain, Nat.ModEq, Nat.digits, False, Eq, HMul.hMul, HMod.hMod, HDiv.hDiv, And.left, List.cons, Eq.mp, And, congrArg, propext, List.isChain_cons_cons, List, Nat.digits_def', Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat and 4 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def Imo2004P6.Nice Digit lists (little-endian) whose entry at each position has the parity of the position, so that consecutive digits have different parity line 48 source
Source documentation
Digit lists (little-endian) whose entry at each position has the parity of the position, so that consecutive digits have different parity.

no axioms what this means
Statement uses: List, Nat
Proof uses: And, Membership.mem, LT.lt, OfNat.ofNat, List.length, Eq, HMod.hMod, GetElem.getElem
6 instances, coercions and auxiliary constants left out.
```
def Nice (L : List ℕ) : Prop :=
…
```
lemma Imo2004P6.Nice.append line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Imo2004P6.Nice, Eq, HMod.hMod, List.length, OfNat.ofNat, HAppend.hAppend
Proof uses: And.intro, Membership.mem, LT.lt, GetElem.getElem, Or, Iff.mp, List.mem_append, And.left, GE.ge, Nat.lt_or_ge, Eq.mpr, id, congrArg, List.getElem_append_left, And.right, HSub.hSub, List.getElem_append_right, Eq.mp, HAdd.hAdd, List.length_append
22 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P6.Nice.snoc line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Imo2004P6.Nice, LT.lt, OfNat.ofNat, Eq, HMod.hMod, List.length, HAppend.hAppend, List.cons, List.nil
Proof uses: And.intro, Membership.mem, GetElem.getElem, Or, Iff.mp, List.mem_append, And.left, Eq.mp, GE.ge, Nat.lt_or_ge, Eq.mpr, id, congrArg, List.getElem_append_left, And.right, HAdd.hAdd, of_eq_true, Eq.trans, True, congrFun' and 6 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P6.Nice.isChain line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Imo2004P6.Nice, List.IsChain, Not, Nat.ModEq, OfNat.ofNat
Proof uses: Eq.mpr, LT.lt, HAdd.hAdd, List.length, GetElem.getElem, id, Eq, congrArg, propext, List.isChain_iff_getElem, HMod.hMod, And.right, Membership.mem, Decidable.byContradiction
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P6.dvd_geom_sum If u is coprime to x and 2 ≤ x, then u divides some sum 1 + x + x ^ 2 + ⋯ + x ^ (t - 1) with 0 < t line 93 source
Source documentation
If u is coprime to x and 2 ≤ x, then u divides some sum 1 + x + x ^ 2 + ⋯ + x ^ (t - 1) with 0 < t.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, LE.le, OfNat.ofNat, Exists, And, LT.lt, Dvd.dvd, Finset.sum, Finset.range, HPow.hPow
Proof uses: Nat.pos_of_ne_zero, Eq, Eq.mp, congrFun', Nat.gcd, congrArg, Eq.trans, Nat.gcd_zero_right, HMul.hMul, HSub.hSub, Nat.mul_pos, Nat.Coprime.mul_right, Nat.dvd_sub, Nat.gcd_dvd_left, Nat.gcd_dvd_right, Iff.mp, Nat.dvd_one, Exists.intro, Nat.totient, And.intro and 12 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_geom_sum {u x : ℕ} (hux : Nat.Coprime x u) (hx : 2 ≤ x) :
    ∃ t, 0 < t ∧ u ∣ ∑ i ∈ Finset.range t, x ^ i := by
…
```
lemma Imo2004P6.nice_flatten_replicate line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Imo2004P6.Nice, Eq, HMod.hMod, List.length, OfNat.ofNat, And, List.flatten, List.replicate, HMul.hMul, Nat.ofDigits, Finset.sum, Finset.range, HPow.hPow
Proof uses: Nat.recAux, And.intro, Membership.mem, LT.lt, GetElem.getElem, of_eq_true, List.nil, Eq.trans, True, forall_congr, False, implies_congr, Eq.refl, implies_true, Eq.substr, id, forall_prop_domain_congr, congrArg, MulZeroClass.zero_mul, eq_self and 40 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P6.exists_alternating_multiple Repeating a Nice digit block of even length enough times produces an alternating multiple of n * u, where n divides the block and u is coprime to 10 line 128 source
Source documentation
Repeating a Nice digit block of even length enough times produces an alternating multiple of n * u, where n divides the block and u is coprime to 10.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, OfNat.ofNat, List, Ne, List.nil, Eq, HMod.hMod, List.length, Imo2004P6.Nice, Dvd.dvd, Nat.ofDigits, Exists, And, Imo2004P6.Alternating, HMul.hMul
Proof uses: LT.lt, List.length_pos_of_ne_nil, LE.le, HPow.hPow, Nat.le_pow, Finset.sum, Finset.range, Imo2004P6.dvd_geom_sum, Nat.Coprime.pow_left, Nat.Coprime.symm, List.flatten, List.replicate, Imo2004P6.nice_flatten_replicate, Eq.mpr, id, congrArg, Nat.mul_pos, List.ne_nil_of_length_pos, List.getLast, GetElem.getElem and 30 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma exists_alternating_multiple {n u : ℕ} (hu : Nat.Coprime u 10)
    {L : List ℕ} (hne : L ≠ [])
    (hlen : L.length % 2 = 0) (hnice : Nice L)
    (hdvd : n ∣ Nat.ofDigits 10 L) :
    ∃ M, Alternating M ∧ n * u ∣ M := by
…
```
Mentions: Imo2004P6.Nice, Imo2004P6.Alternating
lemma Imo2004P6.exists_alt_multiple_of_dvd Any n dividing 2 ^ i * 5 ^ j * u, where u avoids 2 and 5 and some Nice block of even length is divisible by 2 ^ i * 5 ^ j, has an alternating multiple line 164 source
Source documentation
Any n dividing 2 ^ i * 5 ^ j * u, where u avoids 2 and 5 and some Nice block of even length is divisible by 2 ^ i * 5 ^ j, has an alternating multiple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, List, Ne, List.nil, Eq, HMod.hMod, List.length, Imo2004P6.Nice, HMul.hMul, HPow.hPow, Nat.ofDigits, Exists, And, Imo2004P6.Alternating
Proof uses: Nat.Coprime, Iff.mpr, Nat.Prime.coprime_iff_not_dvd, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_2, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Eq.mpr, id, congrArg, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_mul, Nat.Coprime.symm, Nat.Coprime.mul_left and 4 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma exists_alt_multiple_of_dvd {u n i j : ℕ} (hu2 : ¬ 2 ∣ u) (hu5 : ¬ 5 ∣ u)
    {L : List ℕ} (hne : L ≠ []) (hlen : L.length % 2 = 0) (hnice : Nice L)
    (hdvd : 2 ^ i * 5 ^ j ∣ Nat.ofDigits 10 L) (hn : n ∣ 2 ^ i * 5 ^ j * u) :
    ∃ M, Alternating M ∧ n ∣ M := by
…
```
Mentions: Imo2004P6.Nice, Imo2004P6.Alternating
lemma Imo2004P6.two_block For every k there is a Nice digit block of length 2 * k + 2 divisible by 2 ^ (2 * k + 3) line 178 source
Source documentation
For every k there is a Nice digit block of length 2 * k + 2 divisible by 2 ^ (2 * k + 3).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, List, And, Eq, List.length, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Imo2004P6.Nice, Dvd.dvd, HPow.hPow, Nat.ofDigits
Proof uses: Nat.recAux, Exists.intro, List.cons, List.nil, And.intro, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', zero_add, MulZeroClass.mul_zero, eq_self, Membership.mem, LT.lt, HMod.hMod, GetElem.getElem, of_decide_eq_true, id and 75 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
```
lemma two_block (k : ℕ) : ∃ L : List ℕ, L.length = 2 * k + 2 ∧ Nice L ∧
    2 ^ (2 * k + 3) ∣ Nat.ofDigits 10 L := by
…
```
Mentions: Imo2004P6.Nice
lemma Imo2004P6.five_digit_choice line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, And, Membership.mem, Finset, Finset.range, Eq, HMod.hMod, HAdd.hAdd, HMul.hMul
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P6.five_block For every b there is a Nice digit block of length b + 1 divisible by 10 * 5 ^ b (its bottom digit is 0) line 230 source
Source documentation
For every b there is a Nice digit block of length b + 1 divisible by 10 * 5 ^ b (its bottom digit is 0).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, List, And, Eq, List.length, HAdd.hAdd, OfNat.ofNat, Imo2004P6.Nice, Dvd.dvd, HMul.hMul, HPow.hPow, Nat.ofDigits
Proof uses: Nat.recAux, Exists.intro, List.cons, List.nil, And.intro, of_eq_true, Eq.trans, True, congr, congrArg, zero_add, eq_self, Membership.mem, LT.lt, HMod.hMod, GetElem.getElem, of_decide_eq_true, id, Bool, Decidable.decide and 62 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma five_block (b : ℕ) : ∃ L : List ℕ, L.length = b + 1 ∧ Nice L ∧
    10 * 5 ^ b ∣ Nat.ofDigits 10 L := by
…
```
Mentions: Imo2004P6.Nice
lemma Imo2004P6.exists_alternating_multiple' line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, Dvd.dvd, Exists, And, Imo2004P6.Alternating
Proof uses: dite, Nat.Coprime.mul_dvd_of_dvd_of_dvd, of_decide_eq_true, Nat.Coprime, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, HMul.hMul, HPow.hPow, Nat.exists_eq_pow_mul_and_not_dvd, LT.lt.ne', Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Bool.false, GT.gt, Or, Nat.eq_zero_or_pos and 66 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
problem Imo2004P6.imo2004_p6 line 306 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Set, Imo2004P6.SolutionSet, And, LT.lt, OfNat.ofNat, Exists, Imo2004P6.Alternating, HMul.hMul
Proof uses: Iff.intro, Not, Dvd.dvd, And.intro, Imo2004P6.exists_alternating_multiple', Eq, Exists.intro, Eq.symm, Imo2004P6.not_alternating_of_dvd_twenty, Dvd.dvd.mul_right
16 instances, coercions and auxiliary constants left out.

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