The abc conjecture

A claimed proof exists and is not accepted by the wider community — the conjecture's status is genuinely contested.

Inferred from the community field; finer classification has not been reviewed.

0 Submit progress Lean 4 ↓Discussion (0)

Problem statement

For coprime positive integers $a + b = c$ , let $\operatorname{rad}(n)$ denote the product of the distinct primes dividing $n$ . The conjecture asserts that for every $\varepsilon > 0$ there are only finitely many triples with

c > \operatorname{rad}(abc)^{1+\varepsilon}.

Lean 4

Not yet attached

No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.

Share a formalization →Verification guide ↗

Background

Formulated by Oesterlé and Masser in the mid-1980s. Shinichi Mochizuki announced a proof via inter-universal Teichmüller theory in 2012; it was published in Publications of the RIMS in 2021. Peter Scholze and Jakob Stix published a report identifying what they consider a gap in Corollary 3.12, which Mochizuki disputes. No consensus has emerged.

Why it matters

The conjecture implies Fermat's Last Theorem for large exponents, the Mordell conjecture (Faltings' theorem) with effective constants, Roth's theorem, and a long list of Diophantine statements. Its contested status is also a case study in how a community decides that something has been proved.

Known partial results

Weaker exponential bounds are known via Baker's theory of linear forms in logarithms.
The function-field analogue (the Mason–Stothers theorem) is elementary and true.
The dispute is documented publicly: see the Scholze–Stix report and Mochizuki's replies.

References

[1]P. Scholze, J. Stix, Why abc is still a conjecture (report, 2018).

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.