Source labels openChecked July 26, 2026

Catalan's conjecture and related Diophantine equations

Lebesgue-Nagell Equation Conjecture*

Mathematical statement

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

Statement source: Wikipedia statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

lebesgue_nagell

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem lebesgue_nagell (p : ℕ) (hp : p.Prime) (hodd : Odd p) (x y : ℤ) :    x ^ 2 - 2 = y ^ p ↔ (x = 1 ∨ x = -1) ∧ y = -1 := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization arXiv:2507.12397background Wikipedia - Catalan's conjecturebackground