Source labels openChecked July 26, 2026

Catalan's conjecture and related Diophantine equations

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$ .

Number theory AMS 11

Mathematical statement

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$ .

Statement source: Wikipedia statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

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

pillais_conjecture

Canonical source

Complete statement target, proof intentionally absentLean 4

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  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 Wikipedia - Catalan's conjecturebackground arXiv:2507.12397background