abc conjecture

Reference: Wikipedia

def ABC.radical (n : ℕ) : ℕ

The radical of n denoted is the product of the distinct prime factors of n.

Equations

• ABC.radical n = n.primeFactors.prod id

theorem ABC.radical_16 : radical 16 = 2

theorem ABC.radical_17 : radical 17 = 17

theorem ABC.radical_12 : radical 12 = 6

noncomputable def ABC.quality (a b c : ℕ) : ℝ

Quality q(a, b, c) of the triple (a, b, c) is defined as q(a,b,c) = log (c) / log (rad(abc)).

Equations

• ABC.quality a b c = Real.log ↑c / Real.log ↑(ABC.radical (a * b * c))

theorem ABC.abc (ε : ℝ) (hε : 0 < ε) : {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ {a, b, c}.Pairwise Nat.Coprime ∧ a + b = c ∧ ↑(radical (a * b * c)) ^ (1 + ε) < ↑c}.Finite

For every positive real number ε, there exist only finitely many triples (a, b, c) of coprime positive integers, with a + b = c, such that c > rad(abc)^(1+ε)

theorem ABC.abc.variants.lt_constant_mul (ε : ℝ) (hε : 0 < ε) : ∃ (K : ℝ), ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → {a, b, c}.Pairwise Nat.Coprime → a + b = c → ↑c < K * ↑(radical (a * b * c)) ^ (1 + ε)

For every positive real number ε, there exists a constant K_ε such that for all triples (a, b, c) of coprime positive integers, with a + b = c we have c < K_ε rad(abc)^(1+ε).

theorem ABC.abc.variants.quality (ε : ℝ) (hε : 0 < ε) : {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ {a, b, c}.Pairwise Nat.Coprime ∧ a + b = c ∧ ABC.quality a b c > 1 + ε}.Finite

For every positive real number ε, there exist only finitely many triples (a, b, c) of coprime positive integers with a + b = c such that q(a, b, c) > 1 + ε.