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

26 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1992, Problem 1

Find, as a function of n, the sum of the digits of

9 × 99 × 9999 × ... × (10^2ⁿ - 1),

where each factor has twice as many digits as the last one.

Imports (3)

Imported by 1 file

Compfiles.lean

lemma Usa1992P1.digits_pow TODO add a generalization of this mathlib? line 33 source
Source comment
TODO add a generalization of this mathlib?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.length, Nat.digits, OfNat.ofNat, HPow.hPow, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, List.cons, List.nil, List, HMod.hMod, HDiv.hDiv, pow_zero, Nat.digits_of_two_le_of_pos, LE.le, eq_true_of_decide, Eq.refl, Bool, Bool.true, LT.lt, eq_self and 18 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma digits_pow (m : ℕ) : (Nat.digits 10 (10^m)).length = m + 1 := by
…
```
lemma Usa1992P1.lemma2 line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, List.length, Nat.digits, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, Eq, True, congr, congrArg, List, List.nil, Nat.digits_zero, zero_add, eq_self, GT.gt, Or, Nat.eq_zero_or_pos, congrFun', Function.swap, LE.le, or_true, Eq.symm and 14 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Usa1992P1.digits_sum_mul_pow line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.sum, Nat.digits, OfNat.ofNat, HMul.hMul, HPow.hPow
Proof uses: Nat.casesAuxOn, of_eq_true, Eq.trans, True, congr, congrArg, List, List.nil, MulZeroClass.zero_mul, Nat.digits_zero, eq_self, Eq.symm, HAdd.hAdd, Eq.mpr, id, mul_comm, HAppend.hAppend, List.replicate, Nat.digits_base_pow_mul, HDiv.hDiv and 16 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa1992P1.digits_sum line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Eq, List.sum, Nat.digits, HAdd.hAdd, HMul.hMul
Proof uses: Nat.casesAuxOn, of_eq_true, Eq.trans, True, congr, congrArg, List, congrFun', MulZeroClass.zero_mul, zero_add, List.nil, Nat.digits_zero, eq_self, Eq.symm, LE.le, List.length, Usa1992P1.lemma2, Nat.le_of_lt_succ, Exists, Nat.le.dest and 29 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1992P1.Finset.prod_odd line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Nat, Finset, Membership.mem, Odd, Finset.prod
Proof uses: Finset.induction, of_eq_true, EmptyCollection.emptyCollection, OfNat.ofNat, Eq.trans, True, implies_congr, forall_congr, False, Eq.refl, implies_true, Not, Insert.insert, Eq.mpr, HMul.hMul, id, Eq, congrArg, Finset.prod_insert, And and 7 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
example Usa1992P1.(example at line 89) line 89 source
lemma Usa1992P1.lemma3 line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, HMod.hMod, OfNat.ofNat, Eq, List.sum, Nat.digits
Proof uses: Eq.mpr, List.cons, HDiv.hDiv, id, congrArg, List, Nat.digits_eq_cons_digits_div, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, dite, of_eq_true, Eq.trans, True, congr, List.nil, congrFun', zero_add and 7 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Usa1992P1.lemma6 line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, List.Forall₂, LE.le, Nat.ofDigits
Proof uses: List.rec, List.nil, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, id, Eq, Eq.mp, List.cons, False.elim, False, eq_false', noConfusion_of_Nat, List.ctorIdx, And, eq_true, and_true, add_le_add and 3 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Usa1992P1.ofDigits_sub_ofDigits_eq_ofDigits_zipWith The subtraction of ofDigits of two lists is equal to ofDigits of digit-wise subtraction of them line 119 source
Source documentation
The subtraction of ofDigits of two lists is equal to ofDigits of digit-wise subtraction of them

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, List.Forall₂, LE.le, Eq, HSub.hSub, Nat.ofDigits, List.zipWith
Proof uses: List.rec, List.nil, of_eq_true, Eq.trans, OfNat.ofNat, True, congr, congrArg, congrFun', id, Eq.mp, tsub_self, List.map, List.zipWith_self, funext, List.map_nil, eq_self, List.cons, False.elim, False and 15 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem ofDigits_sub_ofDigits_eq_ofDigits_zipWith {b : ℕ} {l1 l2 : List ℕ}
    (hg : List.Forall₂ (· ≤ ·) l1 l2) :
    Nat.ofDigits b l2 - Nat.ofDigits b l1 =
    Nat.ofDigits b (l2.zipWith (· - ·) l1) := by
…
```
lemma Usa1992P1.lemma8 line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HSub.hSub, HPow.hPow, OfNat.ofNat, Nat.ofDigits, List.replicate
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, pow_zero, tsub_self, eq_self, Eq.mpr, HAdd.hAdd, List.cons, id, List, List.replicate_succ, HMul.hMul, Nat.ofDigits_cons, LE.le, Nat.one_le_pow', pow_succ
37 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa1992P1.lemma9 line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, LE.le, List.length, Nat.digits
Proof uses: Iff.mpr, Nat.digits_length_le_iff, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa1992P1.padList line 154 source
no axioms what this means
Statement uses: List, Nat
Proof uses: HAppend.hAppend, List.replicate, HSub.hSub, List.length, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
lemma Usa1992P1.padList_cons line 156 source
standard axioms: propext what this means
Statement uses: Nat, List, Eq, Usa1992P1.padList, List.cons, HAdd.hAdd, OfNat.ofNat
Proof uses: of_eq_true, HAppend.hAppend, List.replicate, HSub.hSub, List.length, Eq.trans, True, congrFun', congrArg, Nat.Simproc.add_sub_add_le, of_decide_eq_true, LE.le, Eq.refl, Bool, Bool.true, eq_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Usa1992P1.digitsPadded line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List
Proof uses: Usa1992P1.padList, Nat.digits
theorem Usa1992P1.digitsPadded_lt_base line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Membership.mem, List, Usa1992P1.digitsPadded
Proof uses: Nat.digits, And, Not, Eq, HSub.hSub, List.length, Or, Eq.mp, HAppend.hAppend, List.replicate, Eq.trans, congrArg, Nat.digits_lt_base
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa1992P1.digitsPaddedLength line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, List.length, Nat.digits, Eq, Usa1992P1.digitsPadded
Proof uses: id, Usa1992P1.padList, Eq.mpr, HAppend.hAppend, List, List.replicate, HSub.hSub, OfNat.ofNat, HAdd.hAdd, congrFun', congrArg, Eq.trans, List.length_append, List.length_replicate, Nat.add_sub_of_le
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa1992P1.exists_prefix line 176 source
standard axioms: Quot.sound, propext what this means
Statement uses: List, Nat, Exists, And, Ne, List.nil, List.getLast, OfNat.ofNat, Eq, HAppend.hAppend, List.replicate
Proof uses: List.rec, of_eq_true, Eq.trans, Not, True, congrArg, funext, False, Eq.substr, eq_self, not_true_eq_false, forall_prop_domain_congr, Eq.refl, List.cons, dite, Exists.intro, eq_false', False.elim, noConfusion_of_Nat, List.ctorIdx and 14 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
theorem Usa1992P1.digitsPadded_ofDigits line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, List, Membership.mem, LE.le, List.length, Eq, Usa1992P1.digitsPadded, Nat.ofDigits, Usa1992P1.padList
Proof uses: Exists, And, Ne, List.nil, List.getLast, HAppend.hAppend, List.replicate, Usa1992P1.exists_prefix, Eq.mpr, id, congrArg, Nat.ofDigits_append_replicate_zero, of_eq_true, Eq.trans, True, forall_congr, implies_congr_ctx, Eq.refl, Or, Not and 22 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Usa1992P1.digitsPadded_sum line 224 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.sum, Usa1992P1.digitsPadded, Nat.digits
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAppend.hAppend, List, List.replicate, HSub.hSub, List.length, OfNat.ofNat, HAdd.hAdd, List.sum_append, HSMul.hSMul, List.sum_replicate, nsmul_zero, add_zero, eq_self
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1992P1.List.map_eq_zip line 228 source
standard axioms: propext what this means
Statement uses: Nat, List, Eq, List.map, List.zipWith, List.replicate, List.length
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.map_nil, List.zipWith_self, eq_self, Eq.mpr, List.cons, HAdd.hAdd, OfNat.ofNat, id, congrFun', List.map_cons, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa1992P1.lemma5 line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Eq, List, Usa1992P1.digitsPadded, HSub.hSub, List.map
Proof uses: Nat.digits, List.replicate, List.length, HAppend.hAppend, Eq.mpr, HAdd.hAdd, id, congrArg, List.length_append, List.length_replicate, LE.le, Usa1992P1.lemma9, Nat.ofDigits, HMul.hMul, Nat.ofDigits_append, Nat.ofDigits_digits, Nat.ofDigits_replicate_zero, MulZeroClass.mul_zero, add_zero, Eq.refl and 46 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
lemma Usa1992P1.List.sum_map_sub_aux line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, List.Forall₂, LE.le, And, Eq, List.sum, List.zipWith, HSub.hSub
14 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa1992P1.List.sum_map_sub line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, List.Forall₂, LE.le, Eq, List.sum, List.zipWith, HSub.hSub
Proof uses: And.left, Usa1992P1.List.sum_map_sub_aux
12 instances, coercions and auxiliary constants left out.
lemma Usa1992P1.lemma4 line 318 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Eq, List.sum, Nat.digits, HSub.hSub, HMul.hMul
Proof uses: Eq.mpr, Usa1992P1.digitsPadded, id, congrArg, Eq.symm, Usa1992P1.digitsPadded_sum, List.map, List, Usa1992P1.lemma5, List.zipWith, List.replicate, List.length, Usa1992P1.List.map_eq_zip, List.Forall₂, LE.le, And, List.get, Fin.mk, propext, List.forall₂_iff_get and 19 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
determine Usa1992P1.solution line 340 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HMul.hMul, OfNat.ofNat, HPow.hPow
7 instances, coercions and auxiliary constants left out.
problem Usa1992P1.usa1992_p1 line 342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.sum, Nat.digits, OfNat.ofNat, Finset.prod, Finset.range, HAdd.hAdd, HSub.hSub, HPow.hPow, Usa1992P1.solution
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, List.cons, List.nil, List, HMod.hMod, HDiv.hDiv, Singleton.singleton, Finset, zero_add, Finset.prod_singleton, pow_zero, pow_one, Nat.digits_of_two_le_of_pos, LE.le, eq_true_of_decide and 96 more
132 instances, coercions and auxiliary constants left out.

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