The abc conjecture
If a + b = c with a, b coprime, then c cannot be much larger than the product of the distinct primes dividing abc.
▸Motivation
Formulated by Masser and Oesterlé in the mid-1980s. It says addition and multiplication cannot conspire: you cannot have high prime powers on all three sides of a + b = c.
It implies Fermat's Last Theorem for large exponents, the Mordell conjecture, and much else — which is a reason for caution as well as interest. Mochizuki announced a proof via inter-universal Teichmüller theory in 2012; it remains not accepted by the wider community, with a specific disputed step identified by Scholze and Stix in 2018.
Masser 1985, Oesterlé 1988. Uses Mathlib's radical.
▸Lean API
import Conjectura.Statements.Mathematics.NumberTheory.AbcConjecture
namespace Conjectura.NT006
/-- Is the abc conjecture true? -/
def goal : Prop := Conjectura.NumberTheory.AbcConjectureProp
end Conjectura.NT006▸Definition2
- abc conjectureConjectura.NumberTheory.AbcConjectureProp
The abc conjecture: for every
ε > 0there is a constantKsuch that whenever coprime positive naturals satisfya + b = c, we havec ≤ K · radical(abc)^(1+ε). It says thata + b = ccannot 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 + ε)- CoprimeNat.Coprime
def
▸Related work1
- Why abc is still a conjecturePeter Scholze, Jakob Stix · 2018
Identifies the specific step in Mochizuki's argument they consider unjustified. The dispute is precisely the kind of thing a kernel-checked statement is meant to make unambiguous.
▸For your AI
I am proving a theorem in Lean 4 and submitting it to Conjectura.
## Problem NT006 — The abc conjecture
If a + b = c with a, b coprime, then c cannot be much larger than the product of the distinct primes dividing abc.
## Environment (fixed — do not assume anything newer)
- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`
If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.
## The exact statement I must prove
```lean
theorem solution : AbcConjectureProp := by
sorry
```
## The file I submit
```lean
import Conjectura.Problems.NT006.Statement
namespace Submission
theorem solution : Conjectura.NT006.goal := by
sorry
end Submission
```
## The Lean definitions of every term in this problem
These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.
### abc conjecture
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.
```lean
Conjectura.NumberTheory.AbcConjectureProp
-- unfolds to:
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 + ε)
```
Defined in this corpus.
### Coprime
def
```lean
Nat.Coprime
```
Defined in Mathlib.
## Rules — submissions violating these are rejected automatically
1. **Do not change the name or type of `solution`.** It must satisfy the
statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
Declaring your own `goal`, or redefining a name it depends on, produces a
proof of a *different* statement and is rejected. This is the single most
common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
`Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
`snake_case` theorem names, `UpperCamelCase` types.
## What I want from you
Here is my argument in informal mathematics:
> [PASTE YOUR PROOF SKETCH HERE]
Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.Submissions are not open yet
Conjectura is in beta. You can read every statement, every definition and the Lean behind them, and download the exact files the checker uses — but proofs are not being accepted yet.
The reason is a deliberate order of operations. Accepting a proof means running a stranger’s code and standing behind a verdict, and no statement here yet carries a researcher’s name. A machine-checked answer to a question nobody has vouched for is worth very little, so the vouching comes first.
The English write-ups are also switched off during the beta. Nothing on this page is generated by a model.
Discussion
- Nothing yet.
Sign in to take part.