The Proof Is Not the Point Anymore

August 10, 2026

intent-formalization autoformalization ai-verification formal-methods machine-verifiable-science

The Proof Is Not the Point Anymore

I’ve started noticing that the code I write matters less than the spec I can’t quite state. I’ll sit down to build something, and the actual coding—the part that used to take hours and require real craft—now takes minutes with an agent doing the typing. What takes the hours now is figuring out, precisely enough that a machine could check it, what I actually meant. The bottleneck moved. It didn’t disappear.

This isn’t just a vibe I have about my own work. It’s the shape of what’s happening at the very top of formal reasoning right now, and mathematics is showing us where the rest of us are headed.

In April 2026, a 23-year-old with no advanced math training fed Erdős Problem #1196—open for almost 60 years—into GPT-5.4 Pro as a single prompt. Eighty minutes later, out came a proof. Not a rehash of known techniques: it introduced something genuinely new, a “downward von Mangoldt Markov chain” that solved the problem by staying inside discrete arithmetic instead of the continuous calculus every human attempt had relied on. Terence Tao and Jared Duker Lichtman spent real effort afterward not proving it, but understanding it—stripping 55 pages of chaotic machine reasoning down into something a person could hold in their head. Lichtman called it a proof from The Book.

That story gets told as a triumph of AI capability, and it is one. But the part I keep turning over is what the humans were doing in it. They weren’t executing logic anymore. They were auditing it, translating a correct-but-alien artifact into something legible, deciding which parts of the insight generalized. Tao’s framing, in a Nature interview earlier this year, is that the mathematician’s job is shifting from hiker to cartographer—not walking the terrain step by step, but surveying what the machine already walked and deciding which parts of the map matter.

Here’s the catch, and it’s the same catch I run into with code: producing a plausible answer got radically cheap, but plausible isn’t correct. The First Proof Challenge—ten fresh, unpublished lemmas handed to AI systems in February 2026, specifically chosen to be impossible to have memorized—showed this starkly. The best public system solved six out of ten. Public consumer models mostly produced confident, fluent, wrong proofs. Confidence and correctness had completely decoupled, and the only way anyone caught the difference was a proof checker like Lean, or a small number of humans willing to grind through the verification by hand. Math has a very rare luxury here: a proof either compiles or it doesn’t. There’s no equivalent oracle for whether the AI-generated invoice-matching script or onboarding flow does what you meant.

That’s the intent gap, and it’s not a new problem—it’s an old problem at a new scale. Code has always been “plausible by construction, not correct by construction.” The difference is that a human reviewing every line used to be the safety net, almost by accident, because someone had to type each one. Once an agent can write, test, and ship a feature end to end, that accidental safety net is gone, and nothing has automatically replaced it. The people working on this—researchers calling it “intent formalization”—are essentially trying to build the Lean checker for ordinary software: postconditions, assertions, formal specs that an AI has to satisfy rather than merely resemble. The honest version of that work admits the real bottleneck isn’t writing the checkable spec, it’s knowing precisely enough what you want to write one. Human intent is messy on purpose. Compressing it into something checkable is the actual skill now, and it’s a skill most of us never had to practice, because we could always just… write the code and see if it felt right.

I think this is why “vibe coding” feels good in the moment and bad a week later. You get the dopamine of a working demo without doing the harder cognitive work of stating, in a form that survives scrutiny, what “working” was supposed to mean. The AI didn’t skip a step you used to do—it skipped the step of you being forced to know what you wanted.

So the question I keep sitting with isn’t “how good will these models get.” It’s simpler and less comfortable: if I can’t state precisely what I want, whose job is it going to be to notice?