A proof can verify without explaining

Here are two proofs of the same theorem. Both are short. Both are correct. And you can check every line of both… with nothing more than a pencil. …

Welcome to Intellectual Instinct. Essays on mathematics, economics, and the ideas underneath, read aloud. Today's essay: A proof can verify without explaining. …

The theorem says: there exist irrational numbers a and b, such that a to the power of b is rational. Proof one. Consider s equals the square root of two, raised to the power of the square root of two. Either s is rational, or it isn't. If s is rational, take a and b both equal to root two… and you're done. If s is irrational, take a equal to s, and b equal to root two. Then a to the b is root-two-to-the-root-two… all raised to root two… which is root two, squared… which is two. Rational. You're done again. Q.E.D. Follow it line by line. You'll agree the theorem is true. But notice what you still don't know: which pair works. The proof splits into two cases, and never tells you which one holds. It certifies that a witness exists… and declines to produce it.

Proof two. Take a equal to root two, and b equal to log base two of nine. Both are irrational: root two by the usual parity argument, and log base two of nine because - if it equaled p over q, for integers p and q, then two to the p would equal nine to the q. An even number, equal to an odd one. Now compute. A to the b works out to nine to the one half… which is three. Rational. Q.E.D. Same theorem. Different residue. This time you're holding the witness, and you're holding the reason it works: exponent arithmetic, plus the fact that powers of two and powers of three never collide. You could generate more examples yourself, right now. That's the test. Proof two gave you a recipe. Proof one gave you a shrug. Logicians have a name for the first kind: a nonconstructive proof. Defined in one line: verification without a witness. And the distinction isn't pedantry. Verification settles whether something is true, given the axioms. Understanding is why it's true, and what it connects to. A proof can deliver the first without the second. Most proofs deliver a mixture. What varies is the ratio.

This stopped being a seminar complaint in 1976, when Appel and Haken announced a proof of the four color theorem: every planar map can be colored with four colors, so that no two neighbors share one. Their published proof reduced the problem to one thousand nine hundred thirty-six configurations… and then checked each one. By computer. That's far more than a person can inspect by hand. By the standards of certification, it held. Later formal work confirmed it. But the reception was unease, not celebration. Was a proof no human could follow still a proof? Underneath that question sat the same split. The computer had delivered verification without understanding. The field banked the theorem… and learned little about why four colors suffice. …

Since then, that tension has been industrialized. On both sides. On the verification side, proof assistants like Lean check arguments with a small trusted kernel, down to the axioms. A community library called mathlib now holds a large and growing share of mathematics, in machine-checked form. The strongest case for the machinery is Thomas Hales and the Kepler conjecture. His 1998 proof mixed prose with so much computation that referees couldn't certify it. So he spent over a decade formalizing every step - the Flyspeck project, finished in 2014. Verification had outgrown the referee. The field's answer was to make the kernel the referee.

On the generation side, machine learning systems now find proofs, not just check them. DeepMind reports that AlphaProof and AlphaGeometry 2 solved four of six I.M.O. 2024 problems - silver-medal standard - with output a kernel accepts. Some of those machine-found proofs are short and illuminating. Others read the way the 1976 computation reads: correct, inspectable in principle… explanatory to no one.

William Thurston described the stakes thirty years ago, in On Proof and Progress in Mathematics. Mathematics, he argued, isn't a stockpile of certified theorems. It's a structure of understanding, held by people - and proofs are how that structure gets built and passed on. Read the present moment through his lens, and both the hype and the dismissal look wrong. Machines are racing ahead on certification. The understanding side doesn't compress at the same rate.

To be fair to the machines: cheap verification is a real gift. Results whose details were a swamp get settled for good, and collaborations can trust each other's contributions at machine speed. But a gift to the archive… isn't a gift to the reader.

Explanation isn't a vibe. The two proofs suggest an operational test - not a formal definition: a proof explains when you can compress it into a move you can reuse on a new problem. Proof two compresses to: pick exponents that cancel the irrationality. You can apply that today. Proof one compresses to: something works; we decline to say what. And Appel and Haken compresses to: the case analysis terminates. True. And unhelpful. That's what Thurston was pointing at. The compressible part is the transferable part. And the transferable part is what the next person builds on.

Verification is getting cheap. Understanding isn't. The 1976 disquiet is now a routine experience, rather than a scandal: the result is banked; the insight is not. The scarce input to mathematics isn't certificates. It's proofs that teach.

So here's the counsel, aimed at whoever hands you the next theorem - human or otherwise. Check the proof the way you checked the two at the top: with a pencil, and a little suspicion. Both will hold up. Only one leaves the pencil in your hand. …

That's the essay. You'll find the text, and everything else, at intellectual-instinct.pages.dev. Music by Kevin MacLeod. Thank you for listening.