abc conjecture
AbcConjecturePropdef
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 + ε)import Conjectura.Statements.Mathematics.NumberTheory.AbcConjecture · maintainer — open · raw source
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