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

13 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2017, Problem 1

For any integer a₀ > 1, define the sequence

aₙ₊₁ = √aₙ, if aₙ is a perfect square or aₙ + 3 otherwise.

Find all values of a₀ for which there exists A such that aₙ = A for infinitely many values of n.

Imports (2)

Imported by 1 file

Compfiles.lean

determine Imo2017P1.solution_set line 36 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Dvd.dvd
3 instances, coercions and auxiliary constants left out.
abbrev Imo2017P1.Rule The recurrence rule defining the sequence line 42 source
Source documentation
The recurrence rule defining the sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: LT.lt, OfNat.ofNat, ite, IsSquare, Eq, HAdd.hAdd, Nat.sqrt
6 instances, coercions and auxiliary constants left out.
```
abbrev Rule (a : ℕ → ℕ → ℕ) : Prop :=
…
```
lemma Imo2017P1.step_sq line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P1.Rule, LT.lt, OfNat.ofNat, IsSquare, Eq, HAdd.hAdd, Nat.sqrt
Proof uses: ite, Eq.mp, congrArg, ite_eq_left
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P1.step_nonsq line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P1.Rule, LT.lt, OfNat.ofNat, Not, IsSquare, Eq, HAdd.hAdd
Proof uses: ite, Nat.sqrt, Eq.mp, congrArg, ite_eq_right
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P1.not_isSquare_of_mod_three line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, OfNat.ofNat, Not, IsSquare
Proof uses: HMul.hMul, False, Or, Eq.mp, congrArg, Nat.mul_mod, False.elim, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_natMod, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Bool, Bool.false, Eq.symm
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P1.one_lt Every term of the sequence is greater than 1 line 66 source
Source documentation
Every term of the sequence is greater than 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, OfNat.ofNat, Imo2017P1.Rule, LT.lt
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, dite, HAdd.hAdd, IsSquare, Nat.sqrt, Imo2017P1.step_sq, HMul.hMul, Eq.rec, LE.le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 70 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma one_lt (ha₀ : ∀ x, a x 0 = x) (ha₁ : Rule a) (hx : 1 < x) :
    ∀ i, 1 < a x i := by
…
```
Mentions: Imo2017P1.Rule
lemma Imo2017P1.three_dvd_iff Divisibility by 3 is invariant along the sequence line 83 source
Source documentation
Divisibility by 3 is invariant along the sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, OfNat.ofNat, Imo2017P1.Rule, LT.lt, Iff, Dvd.dvd
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Iff.rfl, dite, HAdd.hAdd, IsSquare, Nat.sqrt, Imo2017P1.step_sq, Eq.symm, propext, HMul.hMul, Nat.sqrt_eq, Or, Nat.Prime.dvd_mul, Nat.prime_three, And, Not, Iff.mp and 5 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma three_dvd_iff (ha₀ : ∀ x, a x 0 = x) (ha₁ : Rule a) (hx : 1 < x) :
    ∀ i, (3 ∣ a x i ↔ 3 ∣ x) := by
…
```
Mentions: Imo2017P1.Rule
lemma Imo2017P1.run_linear Once the sequence is 2 mod 3, it never again hits a perfect square, so it just increases by 3 forever line 99 source
Source documentation
Once the sequence is 2 mod 3, it never again hits a perfect square, so it just increases by 3 forever.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P1.Rule, LT.lt, OfNat.ofNat, Eq, HMod.hMod, HAdd.hAdd, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, add_zero, MulZeroClass.mul_zero, eq_self, Not, IsSquare, Imo2017P1.not_isSquare_of_mod_three, Eq.mpr, id, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 18 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma run_linear (ha₁ : Rule a) (hx : 1 < x) {i : ℕ} (hi : a x i % 3 = 2) :
    ∀ j, a x (i + j) = a x i + 3 * j := by
…
```
Mentions: Imo2017P1.Rule
lemma Imo2017P1.finite_visits If the sequence is ever 2 mod 3, then it takes each value only finitely often line 114 source
Source documentation
If the sequence is ever 2 mod 3, then it takes each value only finitely often.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P1.Rule, LT.lt, OfNat.ofNat, Eq, HMod.hMod, Set.Finite, Set.ofPred
Proof uses: Set.Finite.subset, Set.Icc, HAdd.hAdd, Set.finite_Icc, Membership.mem, Set, LE.le, Or, Iff.mpr, And, Set.mem_Icc, And.intro, Nat.zero_le, HSub.hSub, HMul.hMul, Imo2017P1.run_linear, Eq.mp, congrArg
24 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma finite_visits (ha₁ : Rule a) (hx : 1 < x) {i : ℕ} (hi : a x i % 3 = 2)
    (A : ℕ) : {n | a x n = A}.Finite := by
…
```
Mentions: Imo2017P1.Rule
lemma Imo2017P1.climb Documented declaration: climb line 130 source
Source documentation
From a value c that is not 2 mod 3, the sequence climbs to the least perfect square in the progression c, c+3, c+6, ..., and the next step takes it down to a value at most √c + 3. (By minimality, no intermediate value of the climb is a square; and the progression does contain a square r² with √c < r ≤ √c + 3, where r is chosen with r² ≡ c (mod 3).)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P1.Rule, LT.lt, OfNat.ofNat, Eq, Ne, HMod.hMod, Exists, LE.le, HAdd.hAdd, Nat.sqrt
Proof uses: And, HMul.hMul, Or, Exists.intro, And.intro, Eq.mpr, id, congrArg, Nat.mul_mod, Eq.refl, Trans.trans, Nat.lt_succ_sqrt, Nat.mul_le_mul, HDiv.hDiv, HSub.hSub, IsSquare, Nat.find, rfl, Nat.recAux, congr and 34 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
```
lemma climb (ha₁ : Rule a) (hx : 1 < x) {i c : ℕ} (hi : a x i = c)
    (hc : c % 3 ≠ 2) : ∃ j, a x j ≤ c.sqrt + 3 := by
…
```
Mentions: Imo2017P1.Rule
lemma Imo2017P1.orbit_min_three If the sequence never hits the class 2 mod 3, then its minimum value is 3 (so that 3 divides every term, and in particular x) line 181 source
Source documentation
If the sequence never hits the class 2 mod 3, then its minimum value is 3 (so that 3 divides every term, and in particular x).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, OfNat.ofNat, Imo2017P1.Rule, LT.lt, Ne, HMod.hMod, And, Dvd.dvd, Exists
Proof uses: Membership.mem, Set, Set.range, LE.le, Exists.intro, InfSet.sInf, And.intro, Nat.sInf_mem, Set.range_nonempty, Nat.sInf_le, rfl, Eq.rec, Imo2017P1.one_lt, Not, IsSquare, HMul.hMul, False, HAdd.hAdd, Eq.mpr, Nat.sqrt and 98 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma orbit_min_three (ha₀ : ∀ x, a x 0 = x) (ha₁ : Rule a) (hx : 1 < x)
    (hno2 : ∀ i, a x i % 3 ≠ 2) : 3 ∣ x ∧ ∃ i, a x i = 3 := by
…
```
Mentions: Imo2017P1.Rule
lemma Imo2017P1.cycle Once the sequence hits 3, it cycles 3 → 6 → 9 → 3 forever line 218 source
Source documentation
Once the sequence hits 3, it cycles 3 → 6 → 9 → 3 forever.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P1.Rule, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Nat.recAux, Eq.mpr, id, congrFun', congrArg, Eq.trans, MulZeroClass.mul_zero, add_zero, Imo2017P1.step_nonsq, Not, IsSquare, Mathlib.Meta.NormNum.not_isSquare_nat_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr and 24 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma cycle (ha₁ : Rule a) (hx : 1 < x) {i : ℕ} (h : a x i = 3) :
    ∀ j, a x (i + 3 * j) = 3 := by
…
```
Mentions: Imo2017P1.Rule, h
problem Imo2017P1.imo2017_p1 line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, OfNat.ofNat, LT.lt, ite, IsSquare, HAdd.hAdd, Nat.sqrt, GT.gt, Iff, Exists, Set.Infinite, Set.ofPred, Membership.mem, Set, Imo2017P1.solution_set
Proof uses: id, Iff.intro, And, Dvd.dvd, And.intro, dite, HMod.hMod, Classical.propDecidable, absurd, Set.Finite, Imo2017P1.finite_visits, Not, And.left, Imo2017P1.orbit_min_three, Eq.mp, Ne, Iff.mpr, Imo2017P1.three_dvd_iff, Exists.intro, Set.infinite_of_injective_forall_mem and 2 more
25 instances, coercions and auxiliary constants left out.

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