FormalConjectures.Wikipedia.ABC

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

abc conjecture

Reference: Wikipedia


namespace ABC

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

def radical (n : ℕ) : ℕ := n.primeFactors.prod id


@[category test, AMS 11]
theorem radical_16 : radical 16 = 2 := by⊢ radical 16 = 2
  have : Nat.primeFactors 16 = {2} := by⊢ radical 16 = 2
    rw [show 16 = 2 ^ 4 by decide, Nat.primeFactors_pow]⊢ Nat.primeFactors 2 = {2}hk⊢ 4 ≠ 0
    ·⊢ Nat.primeFactors 2 = {2} norm_numAll goals completed! 🐙
    ·hk⊢ 4 ≠ 0 decideAll goals completed! 🐙
  norm_num [radical, this]All goals completed! 🐙


@[category test, AMS 11]
theorem radical_17 : radical 17 = 17 := by⊢ radical 17 = 17
  rw [radical, Nat.Prime.primeFactors (by norm_num), Finset.prod_singleton, id]All goals completed! 🐙


@[category test, AMS 11]
theorem radical_12 : radical 12 = 6 := by⊢ radical 12 = 6
  rw [radical, show 12 = 2^2 * 3 by rfl, Nat.primeFactors_mul (by norm_num)
    (by norm_num), Nat.primeFactors_pow _ (by norm_num),
    Nat.Prime.primeFactors (by norm_num), Nat.Prime.primeFactors (by norm_num)]⊢ ({2} ∪ {3}).prod id = 6
  rflAll goals completed! 🐙

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

noncomputable def quality (a b c : ℕ) : ℝ := (c : ℝ).log / (radical <| a * b * c : ℝ).log

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+ε)

@[category research open, AMS 11]
theorem declaration uses 'sorry'abc (ε : ℝ) (hε : 0 < ε) :
    {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ ({a, b, c} : Set ℕ).Pairwise Nat.Coprime ∧
    a + b = c ∧ (radical <| a * b * c : ℝ)^(1 + ε) < c}.Finite := byε:ℝ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
  sorryAll goals completed! 🐙

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+ε).

@[category research open, AMS 11]
theorem declaration uses 'sorry'abc.variants.lt_constant_mul (ε : ℝ) (hε : 0 < ε) : ∃ K,
    ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → ({a, b, c} : Set ℕ).Pairwise Nat.Coprime → a + b = c →
    c < K * (radical <| a * b * c : ℝ)^(1 + ε) := byε:ℝ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 + ε)
  sorryAll goals completed! 🐙

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 + ε.

@[category research open, AMS 11]
theorem declaration uses 'sorry'abc.variants.quality (ε : ℝ) (hε : 0 < ε) :
    {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ ({a, b, c} : Set ℕ).Pairwise Nat.Coprime ∧
    a + b = c ∧ quality a b c > (1 + ε)}.Finite := byε:ℝ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
  sorryAll goals completed! 🐙


end ABC