We Let AI Skip Code Review. Math Didn't.

We Let AI Skip Code Review. Math Didn't.

July 30, 2026
ai-code-review formal-verification intent-formalization lean-proof-assistant agentic-coding

The Gap Between “It Compiles” and “It’s Right”

Every AI coding agent I use now writes, tests, and merges code faster than I can read it, and I’ve noticed I stopped actually reading it. I skim the diff, I see green checkmarks, I approve. That’s not a confession of laziness — it’s what the workflow trains you to do. The agent writes the test, the agent writes the code that passes the test, and I’m left rubber-stamping a system that graded its own homework.

I keep coming back to a question: why does this feel fine when an AI does it for my API endpoints, but it would feel insane if a mathematician announced a new theorem was true because an AI said so and a unit test passed?

Why Math Gets to Trust It

Mathematicians actually do trust AI-generated proofs now — in April 2026, GPT-5.4 Pro produced a full solution to Erdős Problem #1196, a conjecture that had sat unsolved for almost 60 years, in about 80 minutes. Terence Tao and other mathematicians took it seriously enough to spend real effort auditing it, distilling its chaotic 55-page argument into something they could publish as a genuine “Proof from The Book.” That’s a real vote of confidence in AI reasoning at the frontier of a field.

But notice what made that trust earnable: the proof went through Lean. Lean is a formal proof assistant — it doesn’t accept “this looks right” or “the intuition checks out.” It requires every claim to be reduced to primitive logical steps and mechanically verified against the axioms. The AI could hallucinate, ramble, take a bizarre route through probability theory to solve a number theory problem — none of that mattered, because the output had to survive contact with a checker that has no capacity for being persuaded. Mathematics doesn’t trust the AI. It trusts the spec, and the AI’s job is to satisfy the spec.

That’s the part we’ve skipped in software.

“Tests Passed” Is Not “Formally Verified”

When we say an AI coding agent’s output “passed the tests,” we’re leaning on a much weaker guarantee than a Lean-checked proof, and we’re treating it as if it were the same thing. Tests are themselves generated code, often by the same model, often after the fact, often shaped to match whatever the model already produced rather than an independent statement of what the software was supposed to do. That’s not verification — it’s the agent grading its own exam using an answer key it also wrote.

There’s a name for the actual gap here: researchers like Shuvendu Lahiri at Microsoft call it the “intent gap” — the distance between the informal thing you asked for and the precise behavior the code actually implements. In the Codex-autocomplete era, this gap didn’t matter much because a human read every line before it shipped. Human review was the de facto formal check. Agentic coding removed that check, and — this is the part that unsettles me — didn’t replace it with anything nearly as rigorous. AI-generated code, as Lahiri puts it, is “plausible by construction, not correct by construction.” That’s true whether it’s a proof of a number theory conjecture or a rate limiter for your API.

What Intent Formalization Would Actually Look Like

The formal-methods answer to this is something like “intent formalization” — writing down, before generation, a checkable specification of what the code must satisfy: pre/post-conditions, invariants, properties that a verifier (not the model itself) can mechanically check. It’s a spectrum. On the light end, it’s just disambiguating the properties your prompt is vague about via test cases you actually trust. On the heavy end, it’s writing code in something like Dafny or Verus, where the compiler literally won’t accept code that doesn’t satisfy the stated contract — the software equivalent of Lean rejecting an invalid proof.

Notably, even the mathematicians haven’t fully solved this. The First Proof Challenge in February 2026 gave frontier models ten genuinely unpublished lemmas — no contamination possible — and the best public system solved six out of ten, with plenty of confident, wrong proofs along the way. The lesson wasn’t “AI can’t do novel math.” It was that autonomy without a spec to check against produces exactly the kind of plausible nonsense you’d expect, and that grading it without a formal checker required enormous human labor. That’s a preview of what unverified AI code review looks like at scale, except in software the stakes are usually invisible until production.

The Habit We Haven’t Built Yet

I don’t think the answer is “make every engineer learn Lean.” Most software isn’t provable in that sense, and most bugs aren’t from violated logical invariants — they’re from ambiguous intent nobody wrote down. But the mathematicians’ habit is worth stealing in miniature: write the spec before you generate the artifact, and make the spec something other than the model’s own say-so can check.

Right now most of us are doing the equivalent of asking an AI to prove a theorem and accepting it because the proof “sounded right.” Mathematics learned not to do that the hard way. I wonder how expensive our version of that lesson is going to be before we build the same discipline.

Sources

Related

Your AI Passed the Math Test by Proving a Different Theorem

May 5, 2026
formal-verification ai-reasoning specification-problem mathematical-proofs scientific-epistemology

Comments

comments powered by Disqus