Two proofs of the same theorem. Only one leaves you with a move you can reuse.
Here are two proofs of the same theorem. Both are short, both are correct, and you can check every line of both with a pencil.
Theorem. There exist irrational numbers a and b such that a^b is rational.
Proof 1. Consider s = sqrt(2)^sqrt(2). Either s is rational or it isn't. If s is rational, take a = b = sqrt(2) and you're done. If s is irrational, take a = s and b = sqrt(2). Then a^b = (sqrt(2)sqrt(2))sqrt(2) = sqrt(2)^2 = 2, which is rational, and you're done again. QED.
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 says which one holds. It certifies that a witness exists and declines to produce it.
Proof 2. Take a = sqrt(2) and b = log_2(9). Both are irrational: sqrt(2) by the usual parity argument, and log_2(9) because if it equaled p/q for integers p and q, then 2^p = 9^q, an even number equal to an odd one. Now compute: a^b = (2(1/2))(log_2 9) = 2^((1/2) * log_2 9) = 9^(1/2) = 3. Rational. QED.
Same theorem. Different residue.
This time you hold the witness, and you hold 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 2 gave you a recipe. Proof 1 gave you a shrug.
Logicians have a name for the first kind: a nonconstructive proof. Defined in one line: verification without a witness.
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.
The 1976 warning shot
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 1,936 configurations, 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.
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.
Now it's an industry
That tension has since 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, 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 in 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 IMO 2024 problems, at 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.
What explanation is worth
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 2 compresses to "pick exponents that cancel the irrationality." You can apply that today. Proof 1 compresses to "something works; we decline to say what." 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.
The narrow claim
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.
Cross-posted from my site: https://intellectual-instinct.pages.dev/essays/what-is-a-proof-for/
