`Compfiles/Usa2026P4.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 2026, Problem 4

A positive integer n is called solitary if, for any non-negative integers a and b such that a + b = n, either a or b contains the digit "1". Determine, with proof, the number of solitary integers less than 10^2026.

Imports (5)

Imported by 1 file

Compfiles.lean

determine Usa2026P4.solution line 32 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HSub.hSub, HPow.hPow, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
def Usa2026P4.has_digit_one line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Membership.mem, List, Nat.digits, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
def Usa2026P4.is_solitary line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, Or, Usa2026P4.has_digit_one
4 instances, coercions and auxiliary constants left out.
lemma Usa2026P4.digits_def' line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, List, Nat.digits, List.cons, HMod.hMod, HDiv.hDiv
Proof uses: Nat.digits_def', of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.digits_ofDigits line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Membership.mem, LT.lt, OfNat.ofNat, Ne, List.nil, List.getLast, Eq, Nat.digits, Nat.ofDigits
Proof uses: Nat.digits_ofDigits, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.digits_ofDigits' line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Membership.mem, LT.lt, OfNat.ofNat, Eq, Nat.digits, Nat.ofDigits, List.rdropWhile, Decidable.decide
Proof uses: List.reverseRec, List.nil, of_eq_true, Eq.trans, True, congr, congrArg, Nat.digits_zero, List.rdropWhile_nil, eq_self, HAppend.hAppend, List.cons, dite, Eq.mpr, id, List.rdropWhile_concat_pos, rfl, Bool, Eq.symm, List.mem_append_left and 17 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.not_solitary_two_zeros line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Usa2026P4.is_solitary, HMul.hMul, OfNat.ofNat, HPow.hPow
Proof uses: Eq.mpr, And, LT.lt, Eq, HAdd.hAdd, Or, Usa2026P4.has_digit_one, id, congrArg, Usa2026P4.is_solitary.eq_1, Exists, Eq.trans, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Mathlib.Tactic.Push.not_forall_eq, funext, Exists.intro, And.intro, Nat.recAux and 38 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.digit_squeeze line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Set.Ico, HPow.hPow, OfNat.ofNat, HMul.hMul, List, Nat.digits
Proof uses: Nat.recAux, LE.le, LT.lt, List.mem_of_elem_eq_true, rfl, Bool, List.elem, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.natPow_zero, Mathlib.Tactic.IntervalCases.of_le_left, HAdd.hAdd and 15 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.digits_last_mem line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, OfNat.ofNat, LT.lt, HDiv.hDiv, Membership.mem, List, Nat.digits
Proof uses: Nat.recAux, Trans.trans, Nat.pos_of_neZero, Eq.mpr, id, Eq, congrArg, Eq.trans, pow_zero, Nat.div_one, List.cons, HMod.hMod, Usa2026P4.digits_def', Nat.mod_eq_of_lt, Decidable.byContradiction, Not, List.mem_cons_self, HAdd.hAdd, List.mem_cons_of_mem, HMul.hMul and 4 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.zero_lt_mod_ne_zero line 109 source
standard axioms: propext what this means
Statement uses: Nat, Ne, HMod.hMod, OfNat.ofNat, LT.lt
Proof uses: Eq.mpr, id, Eq, congrArg, propext, pos_iff_ne_zero, ne_of_apply_ne
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.digits_div_subset line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, HasSubset.Subset, List, Nat.digits, OfNat.ofNat, HMod.hMod, HPow.hPow, HAdd.hAdd
Proof uses: Nat.recAux, dite, Eq, of_eq_true, Eq.trans, List.nil, True, congrFun', congrArg, Nat.digits_zero, Not, Eq.mpr, List.cons, HDiv.hDiv, id, Usa2026P4.digits_def', Decidable.byContradiction, LT.lt, Membership.mem, And and 22 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.chop_off_leading line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Eq, Nat.ofDigits, HAppend.hAppend, List, List.take, Nat.digits, List.cons, HDiv.hDiv, List.nil
Proof uses: Nat.recAux, And, LE.le, LT.lt, Eq.mpr, id, congrArg, Nat.digits_of_lt, Decidable.byContradiction, Not, of_eq_true, Eq.trans, True, congrFun', pow_zero, Nat.div_one, Nat.ofDigits_singleton, eq_self, HMod.hMod, Usa2026P4.digits_def' and 10 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.solitary_form line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2026P4.is_solitary, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow
Proof uses: And.intro, LT.lt, Eq, HAdd.hAdd, Or, Usa2026P4.has_digit_one, LE.le, Not, Classical.em, Nat.le.intro, Or.inl, Usa2026P4.digit_squeeze, Decidable.byContradiction, Iff.mp, Nat.le_sub_one_iff_lt, Nat.pos_of_neZero, Or.symm, Eq.mpr, id, congrArg and 3 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.solitary_extend line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, HPow.hPow, Iff, Usa2026P4.is_solitary, HAdd.hAdd, HMul.hMul
Proof uses: Mathlib.Tactic.Contrapose.contrapose_iff₁, Iff.intro, Not, Exists, And, Eq, Usa2026P4.has_digit_one, False, Eq.mp, Or, Eq.trans, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, LE.le, List.length, Nat.digits and 95 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 85 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.nines line 230 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, Eq.refl, Eq.mpr, HAdd.hAdd, id, congrArg, add_comm, HAppend.hAppend, List, List.replicate_add, List.cons, List.nil, List.replicate_one, HMul.hMul, List.length, Nat.ofDigits_append, congr, Nat.ofDigits_singleton, Eq.trans, zero_add and 2 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
abbrev Usa2026P4.correction line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Nat.ofDigits, OfNat.ofNat, List.take, List.map, ite, Eq, Nat.digits, HSub.hSub, HPow.hPow
9 instances, coercions and auxiliary constants left out.
lemma Usa2026P4.correction_le line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, LE.le, Usa2026P4.correction, Nat.ofDigits, List.replicate
Proof uses: Nat.casesAuxOn, Eq, le_refl, Eq.symm, Eq.mpr, HSub.hSub, id, congrArg, Usa2026P4.nines, LT.lt, propext, Nat.le_sub_one_iff_lt, Nat.pos_of_neZero, Trans.trans, List.length, List.take, List.map, ite, Nat.digits, rfl and 8 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.nines_sub_correction line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Eq, HSub.hSub, Nat.ofDigits, List.replicate, Usa2026P4.correction, HAppend.hAppend, List, List.map, ite, List.take, Nat.digits, List.length
Proof uses: Eq.mpr, id, congrArg, propext, Nat.sub_eq_iff_eq_add, Usa2026P4.correction_le, Usa2026P4.correction.eq_1, Eq.symm, Nat.ofDigits_append_replicate_zero, List.zipWith, Nat.ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq, of_eq_true, Eq.trans, True, Min.min, congr, congrFun', List.map_take, List.length_append, List.length_take and 21 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.nines_sub_correction_not_has_digit_one line 262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Not, Usa2026P4.has_digit_one, HSub.hSub, Usa2026P4.correction
Proof uses: Nat.casesAuxOn, Eq, of_eq_true, Eq.trans, False, True, congrArg, List, Nat.digits, List.nil, congrFun', pow_zero, tsub_self, zero_tsub, Nat.digits_zero, not_false_eq_true, Eq.symm, Eq.mpr, Nat.ofDigits, List.replicate and 39 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.mem_digits_split line 280 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Iff, And, Not, Membership.mem, List, Nat.digits, HAdd.hAdd, HMul.hMul
Proof uses: Eq, HAppend.hAppend, List.replicate, HSub.hSub, List.length, Nat.digits_append_zeroes_append_digits, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, congrArg, Eq.symm, Eq.mp, Nat.add_sub_of_le, Iff.mpr, LE.le, Nat.digits_length_le_iff and 11 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.one_not_mem_bumped line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Membership.mem, List, Nat.digits, OfNat.ofNat, Nat.ofDigits, List.take, List.map, HAdd.hAdd, ite, Eq, HSub.hSub, HPow.hPow
Proof uses: Eq.mpr, List.rdropWhile, Decidable.decide, id, congrArg, Usa2026P4.digits_ofDigits', And, Exists, LT.lt, Eq.mp, propext, List.mem_map, List.mem_of_mem_take, Nat.digits_lt_base, of_decide_eq_true, Bool, Bool.true, Eq.refl, dite, congrFun' and 13 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.add_correction_not_has_digit_one line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Ne, HDiv.hDiv, HSub.hSub, Not, Usa2026P4.has_digit_one, Usa2026P4.correction
Proof uses: Eq.mpr, List, Nat.digits, id, Eq, congrArg, Usa2026P4.has_digit_one.eq_1, Nat.ofDigits, List.take, List.map, ite, Usa2026P4.correction.eq_1, dite, HAppend.hAppend, List.cons, List.nil, Usa2026P4.chop_off_leading, HMul.hMul, List.length, Nat.ofDigits_append and 63 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.leading_ne_one by lemma 2, we know that 2 is not the leading digit of m line 346 source
Source comment
by lemma 2, we know that 2 is not the leading digit of m

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2026P4.is_solitary, Membership.mem, Finset, Finset.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Ne, HSub.hSub, HMul.hMul, HDiv.hDiv
Proof uses: Mathlib.Tactic.Contrapose.contrapose₃, Eq, Eq.mpr, Not, id, congrArg, Usa2026P4.not_solitary_two_zeros, Or, LT.lt, LE.le, Mathlib.Tactic.Contrapose.contrapose₁, And, Exists, implies_congr, Eq.trans, congr, Mathlib.Tactic.Push.not_forall_eq, funext, Exists.intro, propext and 12 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma leading_ne_one {m k : ℕ} (solitary : is_solitary m)
  (hm : m ∈ Finset.Ico (10 ^ k) (10 ^ (k + 1))) (hm1 : m ≠ 2 * 10 ^ k - 1)
  (hm2 : ∀ n ∈ Finset.Ico 1 (10 ^ k), is_solitary n → m ≠ 2 * 10 ^ k + n)
    : (m - (10 ^ k - 1)) / 10 ^ k ≠ 1 := by
…
```
Mentions: Usa2026P4.is_solitary
lemma Usa2026P4.solitary_iff line 369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Iff, Usa2026P4.is_solitary, Or, Eq, HSub.hSub, HMul.hMul, Exists, And
Proof uses: Iff.intro, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, Ne, id, implies_congr, Eq.trans, congrArg, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, Eq.refl, absurd, False, LT.lt, Usa2026P4.has_digit_one, Mathlib.Tactic.Push.not_forall_eq, funext, Usa2026P4.correction and 21 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Usa2026P4.solitary_count line 395 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset.filter, Usa2026P4.is_solitary, Classical.propDecidable, Finset.Ico, OfNat.ofNat, HPow.hPow, HSub.hSub
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Finset, EmptyCollection.emptyCollection, Finset.filter.congr_simp, Eq.refl, pow_zero, Finset.Ico_eq_empty_of_le, LE.le, Finset.filter_empty, congrFun', tsub_self, eq_self, HAdd.hAdd, Union.union, Eq.mpr and 46 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
problem Usa2026P4.usa2026_p4 line 428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Finset.filter, Usa2026P4.is_solitary, Classical.propDecidable, Finset.Ico, OfNat.ofNat, HPow.hPow, Usa2026P4.solution
Proof uses: Usa2026P4.solitary_count
8 instances, coercions and auxiliary constants left out.

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