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

23 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1988, Problem 3

A function $f$ defined on the positive integers (and taking positive integers values) is given by: f(1) = 1 f(3) = 3 f(2 \cdot n) = f(n) f(4 \cdot n + 1) = 2 \cdot f(2 \cdot n + 1) - f(n) f(4 \cdot n + 3) = 3 \cdot f(2 \cdot n + 1) - 2 \cdot f(n) for all positive integers $n.$ Determine with proof the number of positive integers $\leq 1988$ for which $f(n) = n.$

Imports (5)

Imported by 1 file

Compfiles.lean

determine Imo1988P3.solution line 35 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
def Imo1988P3.binaryReverse Reverse the base-two digits, dropping leading zeroes line 40 source
Source documentation
Reverse the base-two digits, dropping leading zeroes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Nat.ofDigits, OfNat.ofNat, List.reverse, Nat.digits
2 instances, coercions and auxiliary constants left out.
```
def binaryReverse (n : ℕ) : ℕ :=
…
```
lemma Imo1988P3.binaryReverse_pos Positive inputs have positive binary reversals line 44 source
Source documentation
Positive inputs have positive binary reversals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, LT.lt, Nat, OfNat.ofNat, Imo1988P3.binaryReverse
Proof uses: id, Ne, Nat.ne_of_gt, Subtype.property, List, Nat.digits, List.nil, Iff.mpr, Nat.digits_ne_nil_iff_ne_zero, List.sum, List.reverse, Eq.mpr, Eq, congrArg, List.sum_reverse, HAdd.hAdd, Exists, And, Membership.mem, List.sum_pos_iff_exists_pos_nat and 15 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma binaryReverse_pos (n : ℕ+) : 0 < binaryReverse (n : ℕ) := by
…
```
Mentions: Imo1988P3.binaryReverse
def Imo1988P3.pnatBinaryReverse Binary reversal on positive naturals line 55 source
Source documentation
Binary reversal on positive naturals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat
Proof uses: Subtype.mk, Nat, LT.lt, OfNat.ofNat, Imo1988P3.binaryReverse, Imo1988P3.binaryReverse_pos
3 instances, coercions and auxiliary constants left out.
```
def pnatBinaryReverse (n : ℕ+) : ℕ+ :=
…
```
def Imo1988P3.BinaryPalindrome Binary palindromes line 59 source
Source documentation
Binary palindromes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: List.Palindrome, Nat.digits, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def BinaryPalindrome (n : ℕ) : Prop :=
…
```
instance Imo1988P3.instDecidablePredBinaryPalindrome line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidablePred, Nat, Imo1988P3.BinaryPalindrome
Proof uses: id, Decidable, inferInstance, List.Palindrome, Nat.digits, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P3.binaryReverse_fixed_iff_binaryPalindrome line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Eq, Imo1988P3.binaryReverse, Imo1988P3.BinaryPalindrome
Proof uses: id, Iff.intro, List.Palindrome, Nat.digits, OfNat.ofNat, List.Palindrome.of_reverse_eq, Nat.ofDigits_inj_of_len_eq, of_decide_eq_true, LT.lt, Bool, Decidable.decide, Bool.true, Eq.refl, List.reverse, of_eq_true, List.length, Eq.trans, True, congrFun', congrArg and 13 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
structure Imo1988P3.SatisfiesRecurrence The five recurrence clauses from the problem line 86 source
Source documentation
The five recurrence clauses from the problem.

standard axioms: propext what this means
Statement uses: PNat
```
structure SatisfiesRecurrence (f : ℕ+ → ℕ+) : Prop where
…
```
Mentions: f
lemma Imo1988P3.digits_two_mul Append a binary zero line 94 source
Source documentation
Append a binary zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, List, Nat.digits, HMul.hMul, List.cons
Proof uses: Nat.digits_base_mul, of_decide_eq_true, LT.lt, id, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.pos_of_ne_zero
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma digits_two_mul (n : ℕ) (hn : n ≠ 0) :
    Nat.digits 2 (2 * n) = 0 :: Nat.digits 2 n := by
…
```
lemma Imo1988P3.digits_two_mul_add_one Append a binary one line 100 source
Source documentation
Append a binary one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List, Nat.digits, OfNat.ofNat, HAdd.hAdd, HMul.hMul, List.cons
Proof uses: Eq.mpr, HDiv.hDiv, id, Eq.trans, And, congrFun', congrArg, HMod.hMod, Nat.add_comm, Nat.digits_of_two_le_of_pos, of_eq_true, LE.le, LT.lt, Or, True, congr, eq_self, true_or, Nat.add_mul_mod_self_left, Nat.mod_succ and 12 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma digits_two_mul_add_one (n : ℕ) :
    Nat.digits 2 (2 * n + 1) = 1 :: Nat.digits 2 n := by
…
```
lemma Imo1988P3.binaryReverse_two_mul line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, Imo1988P3.binaryReverse, HMul.hMul
Proof uses: id, Eq.mpr, Nat.ofDigits, List.reverse, Nat.digits, List.cons, congrArg, List, Imo1988P3.digits_two_mul, Nat.ofDigits_reverse_zero_cons, Eq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P3.digits_four_mul_add_one line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, List, Nat.digits, HAdd.hAdd, HMul.hMul, List.cons
Proof uses: Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, 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, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.IsNat.of_raw and 6 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P3.digits_four_mul_add_three line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List, Nat.digits, OfNat.ofNat, HAdd.hAdd, HMul.hMul, List.cons
Proof uses: Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, 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, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.IsNat.of_raw and 9 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P3.binaryReverse_four_mul_add_one_recurrence line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, HAdd.hAdd, Imo1988P3.binaryReverse, HMul.hMul
Proof uses: id, Eq.mpr, Nat.ofDigits, List.reverse, Nat.digits, List.cons, congrArg, List, Imo1988P3.digits_four_mul_add_one, HPow.hPow, List.length, Nat.ofDigits_reverse_cons, Nat.ofDigits_reverse_zero_cons, Imo1988P3.digits_two_mul_add_one, congr, congrFun', mul_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr and 27 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P3.binaryReverse_four_mul_add_three_recurrence line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Imo1988P3.binaryReverse, HMul.hMul, OfNat.ofNat
Proof uses: id, Eq.mpr, Nat.ofDigits, List.reverse, Nat.digits, List.cons, congrArg, List, Imo1988P3.digits_four_mul_add_three, HPow.hPow, List.length, Nat.ofDigits_reverse_cons, Imo1988P3.digits_two_mul_add_one, congr, Eq.trans, congrFun', mul_one, Nat.add_assoc, Mathlib.Tactic.Ring.of_eq, Nat.rawCast and 29 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P3.pnatBinaryReverse_satisfiesRecurrence Binary reversal satisfies the recurrence line 141 source
Source documentation
Binary reversal satisfies the recurrence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1988P3.SatisfiesRecurrence, Imo1988P3.pnatBinaryReverse
Proof uses: Imo1988P3.SatisfiesRecurrence.mk, PNat.eq, OfNat.ofNat, PNat, Nat, rfl, HMul.hMul, Imo1988P3.binaryReverse_two_mul, Nat.ne_of_gt, Subtype.property, LT.lt, HAdd.hAdd, id, Eq, Imo1988P3.binaryReverse_four_mul_add_one_recurrence, Imo1988P3.binaryReverse_four_mul_add_three_recurrence
9 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma pnatBinaryReverse_satisfiesRecurrence :
    SatisfiesRecurrence pnatBinaryReverse := by
…
```
Mentions: Imo1988P3.SatisfiesRecurrence, Imo1988P3.pnatBinaryReverse
lemma Imo1988P3.recurrence_step One binary-recursion step of uniqueness line 162 source
Source documentation
One binary-recursion step of uniqueness.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Imo1988P3.SatisfiesRecurrence, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Nat, And
Proof uses: And.intro, Trans.trans, Imo1988P3.SatisfiesRecurrence.double, Eq.symm, add_right_cancel, Eq.mpr, id, congrArg, Imo1988P3.SatisfiesRecurrence.four_one, Eq.refl, Imo1988P3.SatisfiesRecurrence.four_three
26 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma recurrence_step {f g : ℕ+ → ℕ+}
    (hf : SatisfiesRecurrence f) (hg : SatisfiesRecurrence g) (p : ℕ+)
    (hp : f p = g p) (hodd : f (2 * p + 1) = g (2 * p + 1)) :
    f (2 * p) = g (2 * p) ∧
      f (4 * p + 1) = g (4 * p + 1) ∧
      f (4 * p + 3) = g (4 * p + 3) := by
…
```
Mentions: f, Imo1988P3.SatisfiesRecurrence
lemma Imo1988P3.recurrence_unique The recurrence determines the function uniquely line 186 source
Source documentation
The recurrence determines the function uniquely.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Imo1988P3.SatisfiesRecurrence, Eq
Proof uses: Nat, Ne, OfNat.ofNat, Subtype.mk, LT.lt, Nat.pos_of_ne_zero, And, HAdd.hAdd, HMul.hMul, Nat.binaryRecFromOne, False.elim, rfl, And.intro, id, Eq.trans, Imo1988P3.SatisfiesRecurrence.one, Eq.symm, Imo1988P3.SatisfiesRecurrence.three, Bool, Nat.bit and 35 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
lemma recurrence_unique {f g : ℕ+ → ℕ+}
    (hf : SatisfiesRecurrence f) (hg : SatisfiesRecurrence g) :
    ∀ n : ℕ+, f n = g n := by
…
```
Mentions: f, Imo1988P3.SatisfiesRecurrence
lemma Imo1988P3.recurrence_unique_binaryReverse The recurrence solution is binary reversal line 233 source
Source documentation
The recurrence solution is binary reversal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Imo1988P3.SatisfiesRecurrence, Eq, Imo1988P3.pnatBinaryReverse
Proof uses: Imo1988P3.recurrence_unique, Imo1988P3.pnatBinaryReverse_satisfiesRecurrence
```
lemma recurrence_unique_binaryReverse (f : ℕ+ → ℕ+) (hf : SatisfiesRecurrence f) :
    ∀ n : ℕ+, f n = pnatBinaryReverse n :=
…
```
Mentions: f, Imo1988P3.SatisfiesRecurrence, Imo1988P3.pnatBinaryReverse
lemma Imo1988P3.pnatBinaryReverse_fixed_iff_palindrome Fixed points are binary palindromes line 238 source
Source documentation
Fixed points are binary palindromes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Iff, Eq, Imo1988P3.pnatBinaryReverse, Imo1988P3.BinaryPalindrome
Proof uses: Eq.mpr, Nat, Imo1988P3.binaryReverse, id, congrArg, Eq.symm, propext, Imo1988P3.binaryReverse_fixed_iff_binaryPalindrome, Iff.intro, Subtype, LT.lt, OfNat.ofNat, Subtype.ext
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma pnatBinaryReverse_fixed_iff_palindrome (n : ℕ+) :
    pnatBinaryReverse n = n ↔ BinaryPalindrome (n : ℕ) := by
…
```
Mentions: Imo1988P3.pnatBinaryReverse, Imo1988P3.BinaryPalindrome
lemma Imo1988P3.binaryPalindrome_count_le_1988 Count binary palindromes up to 1988 line 244 source
Source documentation
Count binary palindromes up to 1988.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Finset.filter, Imo1988P3.BinaryPalindrome, Finset.Icc, OfNat.ofNat, Imo1988P3.solution
Proof uses: 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 binaryPalindrome_count_le_1988 :
    ((Finset.Icc 1 1988).filter BinaryPalindrome).card = solution := by
…
```
Mentions: Imo1988P3.BinaryPalindrome, Imo1988P3.solution
lemma Imo1988P3.fixedPoint_count_from_recurrence Convert the finite count back to the problem statement line 249 source
Source documentation
Convert the finite count back to the problem statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Imo1988P3.SatisfiesRecurrence, Eq, Nat, Set.ncard, Set.ofPred, And, LE.le, OfNat.ofNat, Imo1988P3.solution
Proof uses: Eq.mpr, Finset.card, Finset.filter, Imo1988P3.BinaryPalindrome, Finset.Icc, id, congrArg, Eq.symm, Imo1988P3.binaryPalindrome_count_le_1988, Finset, Set.ncard_coe_finset, Set.ncard_congr, Membership.mem, Set, propext, Finset.mem_filter, Finset.mem_Icc, And.intro, Subtype.property, LT.lt and 15 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma fixedPoint_count_from_recurrence (f : ℕ+ → ℕ+) (hf : SatisfiesRecurrence f) :
    Set.ncard {n | n ≤ 1988 ∧ f n = n} = solution := by
…
```
Mentions: f, Imo1988P3.SatisfiesRecurrence, Imo1988P3.solution
problem Imo1988P3.imo1988_p3 line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Eq, OfNat.ofNat, Nat, HMul.hMul, HAdd.hAdd, Set.ncard, Set.ofPred, And, LE.le, Imo1988P3.solution
Proof uses: Imo1988P3.fixedPoint_count_from_recurrence, Imo1988P3.SatisfiesRecurrence.mk
21 instances, coercions and auxiliary constants left out.

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