Catalan.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 10 curated AI-written annotations and 7190 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 project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 3 contain sorry, 0 declared as axioms

Catalan's conjecture and related Diophantine equations

References:

Wikipedia - Catalan's conjecture
arXiv:2507.12397 (Lebesgue-Nagell equation)

Imports (1)

FormalConjecturesUtil

theorem Catalan.catalans_conjecture sorry line 38 source
depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HSub.hSub, HPow.hPow, And
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Catalan.pillais_conjecture For positive integers a, b, and c, there are only finitely many positive solutions (x, y, m, n) to the equation $ax^n - by^m = c$ where $(m, n) \neq (2, 2)$ and $x, y > 1$ sorry line 47 source
Source documentation
For positive integers a, b, and c, there are only finitely many positive solutions (x, y, m, n) to the equation $ax^n - by^m = c$ where $(m, n) \neq (2, 2)$ and $x, y > 1$.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Set.Finite, Prod, Set.ofPred, Catalan.pillais_conjecture.match_1, And, Ne, Prod.mk, Eq, HSub.hSub, HMul.hMul, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem pillais_conjecture (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    { (x, y, m, n) : (ℕ × ℕ × ℕ × ℕ) |
      1 < x ∧ 1 < y ∧ 1 < m ∧ 1 < n ∧ (m, n) ≠ (2, 2) ∧
      a * x^n - b * y^m = c }.Finite := by
…
```
Mentions: c
theorem LebesgueNagell.lebesgue_nagell Lebesgue-Nagell Equation Conjecture For any odd prime $p$, the only integer solutions $(x, y)$ to the equation $x^2 - 2 = y^p$ are $(x, y) = (\pm 1, -1)$ sorry line 69 source
Source documentation
Lebesgue-Nagell Equation Conjecture
For any odd prime $p$, the only integer solutions $(x, y)$ to the equation $x^2 - 2 = y^p$ are $(x, y) = (\pm 1, -1)$.
Reference: Ethan Katz and Kyle Pratt, "On the Lebesgue-Nagell equation $x^2 - 2 = y^p$", arXiv:2507.12397

L4DEL explanation
Lebesgue-Nagell Equation Conjecture For any odd prime $p$, the only integer solutions $(x, y)$ to the equation $x^2 - 2 = y^p$ are $(x, y) = (\pm 1, -1)$. Reference: Ethan Katz and Kyle Pratt, "On the Lebesgue-Nagell equation $x^2 - 2 = y^p$", arXiv:2507.12397
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nat, Nat.Prime, Odd, Int, Iff, Eq, HSub.hSub, HPow.hPow, OfNat.ofNat, And, Or, Neg.neg
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lebesgue_nagell (p : ℕ) (hp : p.Prime) (hodd : Odd p) (x y : ℤ) :
    x ^ 2 - 2 = y ^ p ↔ (x = 1 ∨ x = -1) ∧ y = -1 := by
…
```
theorem LebesgueNagell.lebesgue_nagell_solution_pos_one The pair $(1, -1)$ is a solution to $x^2 - 2 = y^p$ for any odd $p$ line 75 source
Source documentation
The pair $(1, -1)$ is a solution to $x^2 - 2 = y^p$ for any odd $p$.

standard axioms: propext what this means
Statement uses: Nat, Odd, Eq, Int, HSub.hSub, HPow.hPow, OfNat.ofNat, Neg.neg
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, congrFun', one_pow, Monoid, HasDistribNeg, Odd.neg_one_pow, eq_self
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lebesgue_nagell_solution_pos_one (p : ℕ) (hodd : Odd p) :
    (1 : ℤ) ^ 2 - 2 = (-1 : ℤ) ^ p := by
…
```
theorem LebesgueNagell.lebesgue_nagell_solution_neg_one The pair $(-1, -1)$ is a solution to $x^2 - 2 = y^p$ for any odd $p$ line 81 source
Source documentation
The pair $(-1, -1)$ is a solution to $x^2 - 2 = y^p$ for any odd $p$.

standard axioms: propext what this means
Statement uses: Nat, Odd, Eq, Int, HSub.hSub, HPow.hPow, Neg.neg, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Even.neg_pow, Even, one_pow, Monoid, HasDistribNeg, Odd.neg_one_pow, eq_self
41 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lebesgue_nagell_solution_neg_one (p : ℕ) (hodd : Odd p) :
    (-1 : ℤ) ^ 2 - 2 = (-1 : ℤ) ^ p := by
…
```