What a proof is for, besides being true

The official job of a proof is certification: the theorem holds, no exceptions, forever. But mathematicians routinely dismiss correct proofs as bad ones, and spend whole careers re-proving what everyone already knows. Whatever a proof is for, being true is only the entry fee.

The first unofficial job is #explanation. The prime number theorem was proved in 1896 with heavy machinery from complex analysis; in 1949, Selberg and @Erdős found an "elementary" proof using nothing beyond the real numbers.¹ Not one new fact was certified — the theorem had been perfectly safe for half a century. The excitement was about something else: learning which parts of mathematics the truth actually depends on. A proof does not just tell you that a theorem holds. It is a map of why.

The second unofficial job is technology. A substantial proof ships machinery — lemmas, definitions, techniques — that outlives its occasion. Wiles's proof of Fermat's Last Theorem matters to almost nobody as a fact about exponents; it matters enormously as a bridge between elliptic curves and modular forms that number theorists now drive across daily. Mathematicians talk about proofs the way engineers talk about factories: the product is nice, but the tooling is the asset.

The four colour test

This is why the #four-colour-theorem caused such unease. Appel and Haken settled it in 1977 by reducing the problem to 1,936 configurations and checking them by computer [2] — over a thousand hours of machine time that no human has ever reviewed end to end.² The discomfort was never really about correctness, which held up under every audit. It was that the community had received a certificate without an explanation: the theorem was now known to be true, and understood not one bit better than the day before.

Set against that, @Lakatos's Proofs and Refutations reads like the other half of the story [1]. His case study is Euler's formula for polyhedra — vertices minus edges plus faces equals two — and the century of monsters that assaulted it: picture frames, cylinders, solids with tunnels through them. Each counterexample forced a sharpening. What, exactly, is a polyhedron? For Lakatos the proof is not the end of inquiry but its instrument: the thing you probe with refutations until the concepts underneath come into focus. Proofs do not merely use definitions. They grow them.

None of this makes computer proof a mistake. #formal-verification provides something human refereeing never has: certainty that scales, indifferent to fatigue and reputation. The honest accounting is that machine proofs are superb at the official job and, so far, mostly silent on the unofficial ones — a certificate factory that ships no tooling. That line may yet blur, as provers begin to surface the intermediate lemmas that make an argument legible to people.

@Thurston kept the ledger plainly: what mathematicians produce is not theorems but human understanding of mathematics, and theorems are how the understanding is invoiced [3].³ That is why an ugly correct proof is a debt, an illuminating one is capital, and "true" was never the interesting compliment.