The Most Productive Failure

Part 4 of five in The Verification Changelog: Five posts reading 2,500 years of mathematics as the release history of one technology, verification, and what that history means for anyone running AI agents unsupervised.

In September 1930, Königsberg hosted two events that should have been scheduled further apart. On September 7, at a small conference on the epistemology of the exact sciences, a 24-year-old logician named Kurt Gödel mentioned, almost in passing, that no formal system for arithmetic can prove all its true statements. Hardly anyone reacted; John von Neumann pulled him aside afterward, and he was about the only one. The next day, in the same city, David Hilbert gave an address whose closing words went out over the radio and now stand on his gravestone: “Wir müssen wissen. Wir werden wissen.” We must know. We will know.

One day. The most confident sentence in the history of mathematics was broadcast one day after the result that would kill its program had been announced, in the same city.

1930 is the year the technology got pointed at itself. It’s worth getting the outcome right, because the popular version of what happened next is wrong in a way that still costs real engineering decisions.

What Hilbert actually ordered

The background was a security incident. In 1901 Bertrand Russell had found a contradiction at the base of Cantor’s set theory: the set of all sets that do not contain themselves breaks the theory outright. Hilbert, whose 23 problems of 1900 had set the century’s agenda, responded like a platform engineer. Formalize all of mathematics in one axiomatic system. Prove, with finitary means everyone accepts, that the system is consistent and complete. And on top of that, the Entscheidungsproblem: a procedure that decides, for any well-formed statement, whether it is provable. Mathematics as a certified codebase with a decision oracle.

Gödel published in 1931: any consistent formal system containing arithmetic is incomplete, there are true statements it cannot prove, and its own consistency is one of them. In 1936, Turing (and Church, independently) pinned down what “procedure” even means and showed the halting problem undecidable. No oracle, not ever. Six years from radio address to rubble.

The wrong lesson

Here is what the theorems of 1931 and 1936 turned into on their way through popular culture: math is broken, formal systems are hopeless, machines can never really do mathematics, human intuition transcends computation. I still meet this reading in engineering discussions. It surfaces as a reason why formal methods “can’t work in principle”, and lately as a shrug at unverifiable AI output. Gödel as a permission slip.

Look at what the theorems actually constrain. Undecidability limits the universal machine, the one that takes any statement whatsoever and decides it. It says nothing about a different task: checking a proof that someone hands you. A proof is a finite chain of inference steps, and whether each step follows the rules of the system is a mechanical question with a terminating answer. Finding a proof is an open-ended search through an infinite space; checking one is bookkeeping. Gödel and Turing drew a boundary between the two, and everything impossible landed on the finding side.

Finding is hard, checking is cheap. I keep that asymmetry pinned over every verification discussion I’m in, because it survived 1931 without a scratch. It is the reason the failure was productive instead of terminal.

Ninety years of the asymmetry paying rent

The checking side is now industrial. Proof assistants like Coq and Lean are exactly the division of labor the asymmetry predicts: a human, or lately a language model, searches for the proof, and a small trusted kernel checks every step. What that unlocked, from the Kepler conjecture to a result a language model found this month, is the next essay’s story. The shape is what matters here: the verifier makes trust in the searcher unnecessary. The searcher can be tired, overconfident, or not human at all. The proof checks or it doesn’t.

Software has a cheaper version of this lesson. A test suite is a checker too, just a weak one: it verifies instances, the cases somebody thought to write down, not the claim. A proof checker verifies the claim, for all inputs, or it rejects. Same boundary, different altitude. Most of engineering still verifies the way Babylonian builders did, by running the thing and seeing whether the granary collapses.

And the rubble of Hilbert’s program organized itself into my industry. Turing’s paper machine became the blueprint of the stored-program computer. Type theory, Russell’s own repair of his paradox, became (via the Curry-Howard correspondence) the theoretical spine of those very proof assistants. Proof theory, invented to secure mathematics, ended up securing compilers. The security project failed and the crash produced computer science. As failures go, the return on this one embarrasses most successes.

Hilbert never conceded, by the way. He was reportedly furious about Gödel’s result, then backed consistency proofs with slightly stronger means (Gentzen delivered one in 1936, at the price of assumptions beyond the finitary). The gravestone sentence stayed. On the checking side of the boundary it even turned out to be plainly true: for any proof actually put in front of us, we can know.

Which is why citing Gödel as the reason a system can’t be verified is a quiet swap: an impossibility about finding, presented as an impossibility about checking. Finding is hard, always was, for humans and machines alike. Checking has been mechanical since before the radio address. Gödel is not an excuse. He is the reason we know exactly where the excuse stops.

The Verification Changelog, part 4 of 5.
← When Physics Was the Test Suite · The Untrusted Searcher →