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

31 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2024, Problem 2

Determine all pairs (a,b) of positive integers for which there exist positive integers g and N such that

gcd(aⁿ + b, bⁿ + a), n = 1, 2, ...

holds for all integers n ≥ N.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2024P2.Condition The condition of the problem line 44 source
Source documentation
The condition of the problem.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: And, LT.lt, OfNat.ofNat, Exists, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow
9 instances, coercions and auxiliary constants left out.
```
def Condition (a b : ℕ) : Prop :=
…
```
lemma Imo2024P2.dvd_pow_iff_of_dvd_sub line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Nat.Coprime, Dvd.dvd, Nat.totient, HSub.hSub, Iff, HAdd.hAdd, HPow.hPow, Eq, ZMod, Units, ZMod.unitOfCoprime, OfNat.ofNat
Proof uses: HMul.hMul, Eq.mpr, Neg.neg, id, congrArg, zpow_add, zpow_mul', Eq.symm, propext, ZMod.natCast_eq_zero_iff, of_eq_true, Eq.trans, True, congr, congrFun', Nat.cast_add, Nat.cast_pow, zpow_natCast, Inv.inv, ZMod.pow_totient and 7 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.a_pos line 62 source
standard axioms: propext what this means
Statement uses: Nat, Imo2024P2.Condition, LT.lt, OfNat.ofNat
Proof uses: And.left, And, Exists, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow
11 instances, coercions and auxiliary constants left out.
lemma Imo2024P2.Condition.b_pos line 64 source
standard axioms: propext what this means
Statement uses: Nat, Imo2024P2.Condition, LT.lt, OfNat.ofNat
Proof uses: And.left, Exists, And, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow, And.right
11 instances, coercions and auxiliary constants left out.
def Imo2024P2.Condition.g The value of g in the problem (determined by a and b) line 67 source
Source documentation
The value of g in the problem (determined by a and b).

standard axioms: Classical.choice, propext what this means
Statement uses: Nat, Imo2024P2.Condition
Proof uses: Exists.choose, Exists, And, LT.lt, OfNat.ofNat, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow
10 instances, coercions and auxiliary constants left out.
```
noncomputable def g : ℕ := h.2.2.choose
```
lemma Imo2024P2.Condition.g_spec line 69 source
standard axioms: Classical.choice, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Exists, And, LT.lt, OfNat.ofNat, Imo2024P2.Condition.g, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow
Proof uses: Exists.choose_spec, And.right
18 instances, coercions and auxiliary constants left out.
def Imo2024P2.Condition.N The value of N in the problem (any sufficiently large value) line 73 source
Source documentation
The value of N in the problem (any sufficiently large value).

standard axioms: Classical.choice, propext what this means
Statement uses: Nat, Imo2024P2.Condition
Proof uses: Exists.choose, And, LT.lt, OfNat.ofNat, Imo2024P2.Condition.g, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow, Imo2024P2.Condition.g_spec
9 instances, coercions and auxiliary constants left out.
```
noncomputable def N : ℕ := h.g_spec.choose
```
lemma Imo2024P2.Condition.N_spec line 75 source
standard axioms: Classical.choice, propext what this means
Statement uses: Nat, Imo2024P2.Condition, And, LT.lt, OfNat.ofNat, Imo2024P2.Condition.g, Imo2024P2.Condition.N, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow
Proof uses: Exists.choose_spec, Imo2024P2.Condition.g_spec
18 instances, coercions and auxiliary constants left out.
lemma Imo2024P2.Condition.g_pos line 78 source
standard axioms: Classical.choice, propext what this means
Statement uses: Nat, Imo2024P2.Condition, LT.lt, OfNat.ofNat, Imo2024P2.Condition.g
Proof uses: And.left, And, Imo2024P2.Condition.N, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow, Imo2024P2.Condition.N_spec
11 instances, coercions and auxiliary constants left out.
lemma Imo2024P2.Condition.N_pos line 80 source
standard axioms: Classical.choice, propext what this means
Statement uses: Nat, Imo2024P2.Condition, LT.lt, OfNat.ofNat, Imo2024P2.Condition.N
Proof uses: And.left, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow, Imo2024P2.Condition.g, And.right, And, Imo2024P2.Condition.N_spec
11 instances, coercions and auxiliary constants left out.
lemma Imo2024P2.Condition.gcd_eq_g line 82 source
standard axioms: Classical.choice, propext what this means
Statement uses: Nat, Imo2024P2.Condition, LE.le, Imo2024P2.Condition.N, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow, Imo2024P2.Condition.g
Proof uses: And.right, LT.lt, OfNat.ofNat, And, Imo2024P2.Condition.N_spec
16 instances, coercions and auxiliary constants left out.
lemma Imo2024P2.Condition.symm line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition
Proof uses: And.intro, LT.lt, OfNat.ofNat, And, Exists, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow, Imo2024P2.Condition.b_pos, Imo2024P2.Condition.a_pos, Exists.intro, Imo2024P2.Condition.g, Imo2024P2.Condition.N, Imo2024P2.Condition.g_pos, Imo2024P2.Condition.N_pos, Eq.mpr, id, congrArg and 2 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.dvd_g_of_le_N_of_dvd line 89 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, LE.le, Imo2024P2.Condition.N, Dvd.dvd, HAdd.hAdd, HPow.hPow, Imo2024P2.Condition.g
Proof uses: Eq.mpr, Nat.gcd, id, Eq, congrArg, Eq.symm, Imo2024P2.Condition.gcd_eq_g, And, propext, Nat.dvd_gcd_iff, And.intro
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.a_coprime_ab_add_one line 96 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, Nat.coprime_one_right_eq_true
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2024P2.Condition.large_n A sufficiently large value of n, congruent to -1 mod φ (a * b + 1) line 100 source
Source documentation
A sufficiently large value of n, congruent to -1 mod φ (a * b + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition
Proof uses: HSub.hSub, HMul.hMul, HAdd.hAdd, Max.max, Imo2024P2.Condition.N, Imo2024P2.Condition.symm, OfNat.ofNat, Nat.totient
8 instances, coercions and auxiliary constants left out.
```
noncomputable def large_n : ℕ := (max h.N h.symm.N + 1) * φ (a * b + 1) - 1
```
lemma Imo2024P2.Condition.symm_large_n line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Eq, Imo2024P2.Condition.large_n, Imo2024P2.Condition.symm
Proof uses: id, HSub, Eq.rec, HSub.hSub, Eq.refl, HMul.hMul, HAdd.hAdd, Max.max, Imo2024P2.Condition.N, OfNat.ofNat, Nat.totient, HMul, Eq.mpr, congrArg, max_comm, mul_comm
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.N_le_large_n line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, LE.le, Imo2024P2.Condition.N, Imo2024P2.Condition.large_n
Proof uses: LT.lt, OfNat.ofNat, Nat.totient, HAdd.hAdd, HMul.hMul, Iff.mpr, Nat.totient_pos, Nat.add_pos_right, zero_lt_one, Eq.mpr, HSub.hSub, Max.max, Imo2024P2.Condition.symm, id, Eq, congrArg, Imo2024P2.Condition.large_n.eq_1, add_mul, one_mul, Nat.add_sub_assoc and 13 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.dvd_large_n_sub_neg_one line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Dvd.dvd, Int, Nat.totient, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HSub.hSub, Imo2024P2.Condition.large_n, Neg.neg
Proof uses: of_eq_true, Eq.trans, Max.max, Imo2024P2.Condition.N, Imo2024P2.Condition.symm, True, congrArg, congrFun', Nat.cast_pred, LT.lt, LE.le, Or, congr, or_self, Function.swap, Nat.cast_mul, Nat.cast_add, Nat.cast_max, Nat.cast_one, sub_neg_eq_add and 1 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2024P2.Condition.large_n_0 A sufficiently large value of n, congruent to 0 mod φ (a * b + 1) line 121 source
Source documentation
A sufficiently large value of n, congruent to 0 mod φ (a * b + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition
Proof uses: HMul.hMul, Max.max, Imo2024P2.Condition.N, Imo2024P2.Condition.symm, Nat.totient, HAdd.hAdd, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
noncomputable def large_n_0 : ℕ := (max h.N h.symm.N) * φ (a * b + 1)
```
lemma Imo2024P2.Condition.symm_large_n_0 line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Eq, Imo2024P2.Condition.large_n_0, Imo2024P2.Condition.symm
Proof uses: id, HMul, Eq.rec, HMul.hMul, Eq.refl, Max.max, Imo2024P2.Condition.N, Eq.mpr, congrArg, max_comm, Nat.totient, HAdd.hAdd, OfNat.ofNat, mul_comm
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.N_le_large_n_0 line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, LE.le, Imo2024P2.Condition.N, Imo2024P2.Condition.large_n_0
Proof uses: LT.lt, OfNat.ofNat, Nat.totient, HAdd.hAdd, HMul.hMul, Iff.mpr, Nat.totient_pos, Nat.add_pos_right, zero_lt_one, Eq.mpr, Max.max, Imo2024P2.Condition.symm, id, Eq, congrArg, Imo2024P2.Condition.large_n_0.eq_1, Nat.le_mul_of_pos_right, LE.le.trans, mul_le_mul', of_eq_true and 6 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.dvd_large_n_0_sub_zero line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Dvd.dvd, Int, Nat.totient, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HSub.hSub, Imo2024P2.Condition.large_n_0
Proof uses: of_eq_true, Eq.trans, Max.max, Imo2024P2.Condition.N, Imo2024P2.Condition.symm, True, congrArg, congrFun', Nat.cast_mul, Nat.cast_max, sub_zero
43 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.ab_add_one_dvd_a_pow_large_n_add_b line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Dvd.dvd, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow, Imo2024P2.Condition.large_n
Proof uses: Eq.mpr, Eq, ZMod, Units, Int, ZMod.unitOfCoprime, Imo2024P2.Condition.a_coprime_ab_add_one, Neg.neg, id, congrArg, propext, Imo2024P2.dvd_pow_iff_of_dvd_sub, Imo2024P2.Condition.dvd_large_n_sub_neg_one, Inv.inv, zpow_neg, zpow_one, mul_add, Eq.trans, Eq.symm, Nat.cast_zero and 14 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.ab_add_one_dvd_b_pow_large_n_add_a line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Dvd.dvd, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow, Imo2024P2.Condition.large_n
Proof uses: Eq.mpr, Imo2024P2.Condition.symm, eq_of_heq, Dvd, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, id, congrArg, mul_comm, Imo2024P2.Condition.symm_large_n, Imo2024P2.Condition.ab_add_one_dvd_a_pow_large_n_add_b
27 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.ab_add_one_dvd_g line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Dvd.dvd, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Imo2024P2.Condition.g
Proof uses: Imo2024P2.Condition.dvd_g_of_le_N_of_dvd, Imo2024P2.Condition.large_n, Imo2024P2.Condition.N_le_large_n, Imo2024P2.Condition.ab_add_one_dvd_a_pow_large_n_add_b, Imo2024P2.Condition.ab_add_one_dvd_b_pow_large_n_add_a
11 instances, coercions and auxiliary constants left out.
lemma Imo2024P2.Condition.ab_add_one_dvd_a_pow_large_n_0_add_b line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Dvd.dvd, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow, Imo2024P2.Condition.large_n_0
Proof uses: Dvd.dvd.trans, Imo2024P2.Condition.g, Imo2024P2.Condition.ab_add_one_dvd_g, Eq.mpr, Nat.gcd, id, Eq, congrArg, Eq.symm, Imo2024P2.Condition.gcd_eq_g, Imo2024P2.Condition.N_le_large_n_0, Nat.gcd_dvd_left
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.ab_add_one_dvd_b_add_one line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Dvd.dvd, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, add_comm, HPow.hPow, Imo2024P2.Condition.large_n_0, Imo2024P2.Condition.ab_add_one_dvd_a_pow_large_n_0_add_b, ZMod, Eq.symm, propext, ZMod.natCast_eq_zero_iff, congrFun', Eq.trans, Nat.cast_add, Nat.cast_one, Eq.mp, Units, Nat.cast_zero, Int and 5 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.a_eq_one line 179 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Eq, OfNat.ofNat
Proof uses: LE.le, HAdd.hAdd, HMul.hMul, Nat.le_of_dvd, Imo2024P2.Condition.ab_add_one_dvd_b_add_one, Eq.mpr, id, congrArg, one_mul, Eq.mp, propext, add_le_add_iff_right, Function.swap, Nat.le_of_mul_le_mul_right, Imo2024P2.Condition.b_pos, LT.lt, Imo2024P2.Condition.a_pos
32 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P2.Condition.b_eq_one line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P2.Condition, Eq, OfNat.ofNat
Proof uses: Imo2024P2.Condition.a_eq_one, Imo2024P2.Condition.symm
1 instances, coercions and auxiliary constants left out.
determine Imo2024P2.solutionSet line 195 source
standard axioms: propext what this means
Statement uses: Set, Prod, PNat
Proof uses: Singleton.singleton, Prod.mk, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
problem Imo2024P2.imo2024_p2 IMO 2024 Problem 2: eventually constant gcd line 197 source
L4DEL explanation
The only pair of positive integers (a, b) for which gcd(a^n + b, b^n + a) is eventually constant is (1, 1).
1. Problem: determine all pairs of positive integers (a, b) such that gcd(a^n + b, b^n + a) takes one constant value g for all n at least some N. The formal answer is solutionSet = {(1, 1)}, stated as membership in solutionSet iff such g and N exist.
2. Solution (complete, no sorry; imported from the Mathlib Archive per the file header): for (1, 1) every term is gcd(2, 2) = 2, so g = 2 and N = 1 work.
3. Conversely, the file works modulo ab+1: for exponents congruent to -1 modulo phi(ab+1) the terms vanish modulo ab+1, so ab+1 divides g and all large terms, hence all terms, which forces a = b = 1.
Prerequisites: Imo2024P2.solutionSet
Sources and attribution: Pinned Lean source (47b19bbfe5f3)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Iff, Membership.mem, Prod, Set, Imo2024P2.solutionSet, Prod.mk, Exists, Nat, LE.le, Eq, Nat.gcd, HAdd.hAdd, HPow.hPow
Proof uses: Iff.intro, OfNat.ofNat, And, Eq.mp, Eq.trans, Singleton.singleton, Prod.mk.injEq, Exists.intro, of_eq_true, True, forall_congr, implies_congr, Eq.refl, congrFun', congrArg, congr, one_pow, Nat.gcd_self, eq_self, implies_true and 12 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
problem imo2024_p2 (a b : ℕ+) :
    (a, b) ∈ solutionSet ↔
    ∃ g N : ℕ+,
      ∀ n : ℕ, N ≤ n → Nat.gcd (a^n + b) (b^n + a) = g := by
…
```
Mentions: Imo2024P2.solutionSet