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
    rw [show 16 = 2 ^ 4 by⊢ radical 16 = 2⊢ Nat.primeFactors 2 = {2}hk⊢ 4 ≠ 0this:Nat.primeFactors 16 = {2}⊢ radical 16 = 2 decideAll goals completed! 🐙⊢ Nat.primeFactors 2 = {2}hk⊢ 4 ≠ 0this:Nat.primeFactors 16 = {2}⊢ radical 16 = 2, Nat.primeFactors_pow⊢ Nat.primeFactors 2 = {2}hk⊢ 4 ≠ 0⊢ Nat.primeFactors 2 = {2}hk⊢ 4 ≠ 0this:Nat.primeFactors 16 = {2}⊢ radical 16 = 2]⊢ Nat.primeFactors 2 = {2}hk⊢ 4 ≠ 0this:Nat.primeFactors 16 = {2}⊢ radical 16 = 2
    ·⊢ Nat.primeFactors 2 = {2}this:Nat.primeFactors 16 = {2}⊢ radical 16 = 2 norm_numAll goals completed! 🐙this:Nat.primeFactors 16 = {2}⊢ radical 16 = 2
    ·hk⊢ 4 ≠ 0this:Nat.primeFactors 16 = {2}⊢ radical 16 = 2 decidethis:Nat.primeFactors 16 = {2}⊢ radical 16 = 2this:Nat.primeFactors 16 = {2}⊢ radical 16 = 2
  norm_num [radical, this]All goals completed! 🐙



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



@[category test, AMS 11]
theorem radical_12 : radical 12 = 6 := by⊢ radical 12 = 6
  rw [radical,⊢ (Nat.primeFactors 12).prod id = 6⊢ ({2} ∪ {3}).prod id = 6 show 12 = 2^2 * 3 by⊢ radical 12 = 6⊢ ({2} ∪ {3}).prod id = 6 rflAll goals completed! 🐙⊢ ({2} ∪ {3}).prod id = 6, Nat.primeFactors_mul (by⊢ 2 ^ 2 ≠ 0⊢ ({2} ∪ {3}).prod id = 6 norm_numAll goals completed! 🐙⊢ ({2} ∪ {3}).prod id = 6)
    (by⊢ 3 ≠ 0⊢ ({2} ∪ {3}).prod id = 6 norm_numAll goals completed! 🐙⊢ ({2} ∪ {3}).prod id = 6), Nat.primeFactors_pow _ (by⊢ 2 ≠ 0⊢ ({2} ∪ {3}).prod id = 6 norm_numAll goals completed! 🐙⊢ ({2} ∪ {3}).prod id = 6),
    Nat.Prime.primeFactors (by⊢ Nat.Prime 2⊢ ({2} ∪ {3}).prod id = 6 norm_numAll goals completed! 🐙⊢ ({2} ∪ {3}).prod id = 6), Nat.Prime.primeFactors (by⊢ Nat.Prime 3⊢ ({2} ∪ {3}).prod id = 6 norm_numAll goals completed! 🐙⊢ ({2} ∪ {3}).prod id = 6)]⊢ ({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 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 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 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