The New Bottleneck Isn't Writing Code, It's Specifying It

August 3, 2026

intent-formalization agentic-ai autoformalization ai-mathematics specification-driven-development

I’ve noticed I spend less time reviewing the code my AI agent writes and more time writing down what “correct” even means before I let it start. That’s a strange sentence to type as someone who spent fifteen years priding himself on writing clean code by hand. But the actual bottleneck in my day has moved somewhere upstream, and I don’t think I built the muscle for where it moved to.

Math got there first

The clearest place to watch this shift happen isn’t in a startup’s codebase — it’s in mathematics, because math has something almost no other field has: a way to check an answer without asking a human. A proof written in Lean either compiles or it doesn’t. There’s no code review, no staging environment, no “looks right to me.” That property is what makes math the canary for what’s coming everywhere else.

In April 2026, a 23-year-old with no formal math training fed Erdős Problem #1196 — open for almost sixty years — into GPT-5.4 Pro as a single prompt. Eighty minutes later, out came a proof. Not a rehash of known techniques either: it introduced a genuinely new object, a “downward von Mangoldt Markov chain,” that sidestepped the precision losses that had stumped human mathematicians working in continuous calculus. The model stayed in discrete arithmetic the whole time and found a mechanism nobody had written down before.

Here’s the part that matters more than the proof itself, though. The raw output was 55 pages of chaotic, barely-parseable reasoning. It took Terence Tao and Jared Duker Lichtman — genuine Fields-Medal-caliber minds — to go in and distill it into something a human could actually hold in their head. Tao didn’t write the proof. He edited it. He decided which parts of the machine’s reasoning were the real insight and which were noise. That’s not calculation. That’s curation, and it’s a completely different skill than the one graduate students spend a decade building.

Plausible isn’t the same as correct

This is where it connects back to code, and where it gets less comfortable. Researchers at Microsoft describe something they call the “intent gap” — the distance between what you meant and what the AI actually built. The uncomfortable line from their work: AI-generated code is “plausible by construction, not correct by construction.” It looks right. It compiles. It passes the obvious tests. Whether it does what you actually wanted is a separate question entirely, and increasingly nobody is answering it, because the whole point of an agentic tool is that you stopped reading every line.

In the old world, that was fine, because a human reviewed each diff and the review was the specification check. Take the human out of that loop — which is the entire premise of the agent products we’re all shipping right now — and the safeguard just disappears. Nothing replaces it unless you build something to replace it.

The replacement, it turns out, is writing down intent as something checkable. That’s a spectrum, not a switch: on the light end, a test suite that pins down the ambiguous edges of a vague prompt. On the heavy end, actual formal specifications in verification-aware languages — pre- and post-conditions the compiler enforces, not just runs. I’ve started doing a version of the light end reflexively before I hand anything nontrivial to an agent, and it’s slower going in and dramatically faster coming out, because the failure mode shifts from “silently wrong” to “won’t compile.”

Grounding, not hype

It would be easy to read the Erdős story and conclude autonomous AI research is basically solved. It isn’t. A month after that proof, eleven mathematicians ran an experiment called the First Proof Challenge: ten genuinely unpublished lemmas, guaranteed absent from any training set, one week, no help. Public models solved two, and mostly the two that resembled things they’d seen before. The best system, from a research group at ETH Zurich, got six. Private frontier models claimed six too, with real disagreement about whether “autonomous” was even the right word for how they got there.

So the capability is real and the ceiling is much lower than the headline result suggests. Both things are true. What’s consistent across both the triumph and the near-misses is where the human work actually landed — not in the step-by-step execution, but in deciding what counted as a real result, auditing the output, and knowing which direction was worth pointing the machine in at all.

I keep coming back to the word cartographer, which Tao used to describe the new job description. Not the one walking the terrain — the one deciding which terrain is worth mapping, and trusting the drone to do the walking. I didn’t train for that job. Almost none of us did. The question I don’t have a clean answer to yet is whether “formalizing intent” is a skill you can pick up the way you picked up a new language, or whether it’s closer to mathematical taste — something that only shows up after you’ve done the slow, unassisted version long enough to know what you’re actually asking for.