abc conjecture

Conjectura.Statements.Mathematics.NumberTheory.AbcConjecture

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.RingTheory.Radical.Basic
import Mathlib.RingTheory.UniqueFactorizationDomain.Nat
import Mathlib.Analysis.SpecialFunctions.Pow.Real

/-! # abc conjecture

Uses Mathlib's `radical` — the product of the distinct prime factors — rather than
defining our own. See `to_review/19-library-conventions.md`. -/

namespace Conjectura.NumberTheory

open UniqueFactorizationMonoid

/-- The **abc conjecture**: for every `ε > 0` there is a constant `K` such that whenever
coprime positive naturals satisfy `a + b = c`, we have `c ≤ K · radical(abc)^(1+ε)`. It says
that `a + b = c` cannot be built out of high prime powers on all three sides at once. -/
def AbcConjectureProp : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ K : ℝ, ∀ a b c : ℕ, 0 < a → 0 < b → Nat.Coprime a b → a + b = c →
    (c : ℝ) ≤ K * (radical (a * b * c) : ℕ) ^ (1 + ε)

end Conjectura.NumberTheory