The abc conjecture

The abc conjecture of Masser and Oesterlé: for every ε > 0 there is a constant C such that every triple of coprime integers a + b = c satisfies

max(|a|, |b|, |c|) ≤ C · rad(a b c) ^ (1 + ε),

where rad n is the product of the distinct primes dividing n. This file states the conjecture as the proposition TauCeti.AbcConjecture, and proves that two other common formulations are equivalent to it. It does not prove the conjecture.

The statement allows any signs, and zero. Coprimality of a and b makes a, b and c pairwise coprime. When one of them vanishes the other two are ±1, and the bound holds once C ≥ 1. Otherwise two of a, b and -c have the same sign, and their absolute values add up to the absolute value of the third. So every such triple is, up to order and signs, a triple of coprime positive integers x + y = z with the same radical, and z is the largest of the three absolute values. The conjecture is therefore equivalent to its form for positive integers (TauCeti.abcConjecture_iff_nat).

The statement ABC.abc of the formal-conjectures project has another shape: for every ε > 0, only finitely many triples of pairwise coprime positive integers a + b = c have rad(a b c) ^ (1 + ε) < c. Its radical n.primeFactors.prod id is Mathlib's UniqueFactorizationMonoid.radical on ℕ (Nat.radical_eq_prod_primeFactors). That statement is equivalent to TauCeti.AbcConjecture too (TauCeti.abcConjecture_iff_forall_finite). A bound with constant C at the exponent 1 + ε / 2 leaves as exceptions at the exponent 1 + ε only triples with rad(a b c) ^ (ε / 2) < C, and these have bounded c. Conversely, the largest c among the finitely many exceptions at the exponent 1 + ε is a constant for that exponent.

The weaker statements with 1 + ε replaced by κ + ε for a fixed κ ≥ 1 are the abc conjecture with exponent κ, TauCeti.AbcConjectureWithExponent κ. Szpiro's conjecture implies the one with exponent 3 / 2, through the Frey curve (TauCeti.AlgorithmicSzpiroConjecture.abcConjectureWithExponent).

Main definitions

• TauCeti.AbcConjecture: the abc conjecture.
• TauCeti.AbcConjectureWithExponent κ: the abc conjecture with exponent κ.

Main results

• TauCeti.abcConjecture_iff_nat: the conjecture is its form for coprime positive integers a + b = c, bounding c.
• TauCeti.abcConjecture_iff_forall_finite: the conjecture is the statement that, for every ε > 0, only finitely many triples have rad(a b c) ^ (1 + ε) < c.
• TauCeti.AbcConjectureWithExponent.mono: a larger exponent gives a weaker statement.
• TauCeti.abcConjectureWithExponent_iff_nat: for every real κ, the abc conjecture with exponent κ is its form for coprime positive integers, of which TauCeti.abcConjecture_iff_nat is the case κ = 1.

References

• D. W. Masser, Open problems, in Proceedings of the Symposium on Analytic Number Theory (W. W. L. Chen, ed.), Imperial College, London, 1985.
• J. Oesterlé, Nouvelles approches du « théorème » de Fermat, Séminaire Bourbaki, exposé 694 (1988), Astérisque 161–162, 165–186.
• The formal-conjectures project, FormalConjectures/Wikipedia/ABC.lean, theorem ABC.abc (github.com/google-deepmind/formal-conjectures @ 817d8a74, Apache-2.0).

def TauCeti.AbcConjectureWithExponent (κ : ℝ) : Prop

The abc conjecture with exponent κ: for every ε > 0 there is a constant C such that max(|a|, |b|, |c|) ≤ C · rad(a b c) ^ (κ + ε) for all coprime integers a and b with a + b = c. The radical is taken in ℕ, of |a b c|. The abc conjecture is the case κ = 1 (TauCeti.AbcConjecture), and the statement becomes weaker as κ grows (TauCeti.AbcConjectureWithExponent.mono).

theorem TauCeti.abcConjectureWithExponent_iff (κ : ℝ) : AbcConjectureWithExponent κ ↔ ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), ∀ (a b c : ℤ), IsCoprime a b → a + b = c → ↑(max (max a.natAbs b.natAbs) c.natAbs) ≤ C * ↑(UniqueFactorizationMonoid.radical (a * b * c).natAbs) ^ (κ + ε)

The abc conjecture with exponent κ, unfolded.

def TauCeti.AbcConjecture : Prop

The abc conjecture (Masser, Oesterlé): for every ε > 0 there is a constant C such that max(|a|, |b|, |c|) ≤ C · rad(a b c) ^ (1 + ε) for all coprime integers a and b with a + b = c. It is the abc conjecture with exponent 1.

theorem TauCeti.abcConjecture_iff : AbcConjecture ↔ ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), ∀ (a b c : ℤ), IsCoprime a b → a + b = c → ↑(max (max a.natAbs b.natAbs) c.natAbs) ≤ C * ↑(UniqueFactorizationMonoid.radical (a * b * c).natAbs) ^ (1 + ε)

The abc conjecture, unfolded.

theorem TauCeti.AbcConjectureWithExponent.mono {κ κ' : ℝ} (h : AbcConjectureWithExponent κ) (hκ : κ ≤ κ') : AbcConjectureWithExponent κ'

The abc conjecture with a larger exponent is weaker: a bound with exponent κ + ε gives one with exponent κ' + ε for every κ' ≥ κ, since the radical is at least 1.

theorem TauCeti.abcConjectureWithExponent_iff_nat (κ : ℝ) : AbcConjectureWithExponent κ ↔ ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), ∀ (a b c : ℕ), 0 < a → 0 < b → a.Coprime b → a + b = c → ↑c ≤ C * ↑(UniqueFactorizationMonoid.radical (a * b * c)) ^ (κ + ε)

The abc conjecture with exponent κ for positive integers: it is equivalent to ask, for every ε > 0, for a constant C with c ≤ C · rad(a b c) ^ (κ + ε) for all coprime positive integers a and b with a + b = c.

theorem TauCeti.abcConjecture_iff_nat : AbcConjecture ↔ ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), ∀ (a b c : ℕ), 0 < a → 0 < b → a.Coprime b → a + b = c → ↑c ≤ C * ↑(UniqueFactorizationMonoid.radical (a * b * c)) ^ (1 + ε)

The abc conjecture for positive integers: it is equivalent to ask, for every ε > 0, for a constant C with c ≤ C · rad(a b c) ^ (1 + ε) for all coprime positive integers a and b with a + b = c.

theorem TauCeti.abcConjecture_iff_forall_finite : AbcConjecture ↔ ∀ (ε : ℝ), 0 < ε → {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ {a, b, c}.Pairwise Nat.Coprime ∧ a + b = c ∧ ↑(UniqueFactorizationMonoid.radical (a * b * c)) ^ (1 + ε) < ↑c}.Finite

The abc conjecture as finitely many exceptions, the form of ABC.abc in the formal-conjectures project: it is equivalent to ask that, for every ε > 0, only finitely many triples of pairwise coprime positive integers a + b = c have rad(a b c) ^ (1 + ε) < c.