Two structures sit on top of the integers: addition and multiplication. Each is simple on its own, yet they barely speak to each other — knowing the prime factorizations of $a$ and $b$ tells you almost nothing about the factorization of $a+b$. Nearly every hard problem in number theory grows out of that crack.
The abc conjecture is the strongest single sentence anyone has written about it: addition and multiplication cannot conspire. A number is "tidy" multiplicatively when it is built from a few primes raised to high powers — a lot of size from very little raw material, which is extravagant. The conjecture says: once $a+b=c$ ties three numbers together, they are not allowed to be that extravagant all at once.
The radical $\operatorname{rad}(n)$ is the product of the distinct primes dividing $n$ — flatten every exponent to 1. So $\operatorname{rad}(72)=\operatorname{rad}(2^3\cdot 3^2)=6$. It records which primes took part, never how deeply.
Here $\varepsilon$ is any small positive number and $K_\varepsilon$ a constant depending only on $\varepsilon$. A small $\operatorname{rad}(abc)$ is exactly the measure of "all three are multiplicatively tidy." So the inequality says: $c$ cannot greatly exceed the raw material it was built from. Exceptions do exist — $1+8=9$ while $\operatorname{rad}(1\cdot8\cdot9)=6<9$ — but only finitely many for each $\varepsilon$.
It is a load-bearing beam: once it stands, everything hanging from it follows for free — Fermat's Last Theorem (for large enough exponents), Roth's approximation theorem, the Mordell conjecture, the Szpiro conjecture. One inequality subsumes half of Diophantine analysis. Most conjectures are leaves; abc is a trunk — and its content is plain enough to explain to a schoolchild.
An effective form of abc would give computable bounds on the solutions of Diophantine equations — "check this far and you are done," precisely what computational number theory has always lacked. The Szpiro conjecture it implies constrains the ratio of discriminant to conductor of an elliptic curve, the very quantities weighed when choosing elliptic-curve cryptography parameters.
More famous is the deadlock it produced. In 2012 Shinichi Mochizuki released five hundred-odd pages of Inter-universal Teichmüller theory claiming a proof; in 2018 Scholze and Stix, after meeting him in person, identified an unbridgeable gap in Corollary 3.12, which Mochizuki rejects; in 2021 the papers appeared in a journal he edits. The mainstream still has not accepted it. This is not "we don't know whether it's right" — it is a community unable to reach consensus, a rare failure mode in mathematics.
A proof in a paper is a persuasive text written for humans: the author is betting the reader will nod at every "clearly." A formalized proof is written for a machine that knows only axioms and inference rules — every step must be mechanically checkable, and the word "clearly" does not exist. The first is an essay; the second is a program that compiles.
The key design is the trusted kernel. However elaborate the automation, however clever the AI search, all of it must ultimately emit a proof term handed to a small kernel — a few thousand lines, read and re-read by many people — which checks it line by line. So you need not trust the AI. You need only trust that little box.
The foundation is the Curry–Howard correspondence:
Read it this way: the proposition $P$ is simultaneously a type, and the proof $p$ is simultaneously a program term of that type; "$P$ is provable" becomes "the type $P$ is inhabited." The payoff is decisive: "is this proof correct?" degenerates into "does this type-check?" — something computers are extremely good at, and can get deterministically right.
It carves out of social consensus a mechanically verifiable core of mathematical truth — and, in the same motion, measures how much human proofs leave out. The ratio of formalized text to original is called the de Bruijn factor; once in the dozens, it is now down to single digits in mature areas. That falling number is the machine gradually learning what humans leave unsaid — a philosophical question you can put a number on, which is very rare.
The 1976 four-colour theorem rested on a machine enumerating 1,936 configurations and triggered the argument "does that even count as a proof?" After four years of refereeing, Hales's proof of the Kepler sphere-packing conjecture drew only "99% certain" from the referees; he then spent eleven years formalizing it (Flyspeck, finished 2014). The turning point was Scholze's 2021 Liquid Tensor Experiment: unsure of the single most delicate step in his own new proof, he handed it to the Lean community, and it checked out within six months — the first time formalization served as live quality control on frontier research.
Industry runs on the same machinery: the correctness of the CompCert compiler and the seL4 microkernel are machine-checked theorems. On the AI side, Lean supplies something reinforcement learning rarely gets — a hallucination-free reward signal: the proof either compiles or it does not.
You compute a number: $1.20205690315959\ldots$, and have no idea what it is. Feed it to an integer-relation engine and the machine replies that it is very likely $\zeta(3)$. You have proved nothing — but you now know what to try to prove.
This is how physicists work, and the axiomatic narrative of the twentieth century hid it from view. Euler computed $\zeta(2)$ to many digits, recognized $\pi^2/6$, and only then went looking for a proof. Experimental mathematics merely re-legitimizes the logic of discovery; it never pretends to be the logic of justification.
The core tool is integer relation detection: given reals $x_1,\dots,x_n$ (computed to hundreds of digits), find integers $a_1,\dots,a_n$, not all zero, with
The PSLQ and LLL algorithms find such a relation in polynomial time, when one exists and the precision suffices. The use is direct: let the $x_k$ be powers of the constant under study, or a basket of known constants; the moment the machine emits integer coefficients, you have guessed a closed form. Precision is the microscope here: too few digits and real relations stay invisible; enough digits and spurious ones become all but impossible.
The prettiest catch is the 1995 BBP formula, found by PSLQ and proved only afterwards:
The $16^{-k}$ is the whole point: it lets you compute the $n$-th hexadecimal digit of $\pi$ without computing any of the digits before it. In two thousand years nobody imagined this was possible — because nobody had a reason to. What found it was not insight but search: search too can strike structure lying outside human imagination.
The OEIS (On-Line Encyclopedia of Integer Sequences) does this daily: throw in a string of numbers, get back the combinatorial object behind it. In theoretical physics, closed forms for Feynman integrals are often guessed by numerical identification (multiple zeta values) and derived rigorously afterwards. In 2021 DeepMind, with mathematicians at Oxford and Sydney, used neural networks to surface a strong dependence in large datasets of knot invariants, from which a new theorem was conjectured and then humanly proved — the machine is not the prover but the conjecture generator: it points a direction through high-dimensional data, the human supplies the reason.
We treat "proof" as an objective object. In practice a proof is accepted because enough competent people read it and believed it — a social process. Three pressures are squeezing that process at once. Proofs are too long (the classification of finite simple groups spans hundreds of papers and nearly ten thousand pages, some authors now dead); too machine-made (nobody can read the enumerations behind four colours or Kepler); too private (a mere handful claim to understand IUT).
Separate three things that get conflated:
Gödel's completeness theorem gives $\vdash\varphi \leftrightarrow \models\varphi$ inside first-order logic. But $\mathsf{Acc}$ is never $\vdash$: no real paper is written as a formal derivation. All of mathematical practice lives in that gap.
Admitting the gap does not weaken mathematics; it explains its efficiency. Omission is exactly what makes human mathematics readable — a fully formalized text is unimpeachably correct and nearly impossible to read. Mathematics has always chased two goals, certainty and understanding, and for centuries a single act (writing a proof) delivered both as a side effect, so nobody noticed they were two things. Machines have pulled them apart for the first time — that is where the frontier really lies.
The shape is already visible. AlphaGeometry and AlphaProof reach silver-medal level on IMO problems, and their reliability comes from Lean's mechanical checking rather than the model's confidence. Terence Tao's Equational Theories Project settled over twenty million implications in a matter of weeks using Lean plus crowdsourcing plus AI — collaboration at that scale simply was not a viable form of organization in the pen-and-paper era. Tao calls it "industrial-scale mathematics": humans ask, decompose and exercise taste; machines enumerate and verify.