The free retry

Ask a programmer about the afternoon they stopped typing and stared at the wall for an uncomfortable period of time. Most have one. It usually comes while watching an agent write code, run the tests, fail, fix it and run them again, faster than they could check the results. Getting it wrong had stopped costing anything. As they contemplate the wallpaper, they realise there's good and bad to all this. The good part: an idea arrives while walking the dog, they have a chat with Claude, and there's a working prototype waiting when they get home. The bad: if they sell their expertise by the hour, an hour no longer measures what it used to.

In September 2026, mathematicians had their own wall-staring afternoon. Anthropic announced a computer-checked proof of Fermat's Last Theorem. OpenAI claimed a blow-up result for the Navier-Stokes equations, a Millennium Prize problem. Charles Fefferman, who wrote the Clay Institute's description of the problem, was "thrilled". Terence Tao warned that "the indiscriminate strip-mining of open problems for solutions may destroy the ecosystem". The mathematician Kirwin Hampshire put the economics in six words: "Mathematicians are paid to prove theorems."

Look closer at Fermat, though. Andrew Wiles proved it in 1995, after a couple of false starts. Claude found nothing new - dozens of agents spent eleven days rebuilding the result in 13 million lines of Lean, which is a programming language for mathematics. Each line is one logical step, and each step must rest on a definition or a result already established. Nothing compiles until the computer has checked everything. What is new is the verification. Maths did not get easier - it just got turned into code.

That is why these fields were the first ones to fall to AI. Each now offers the free retry - an attempt can fail inside a controlled environment, and an automated check can reject it before anyone acts on the result. The compute isn’t free - Fermat took dozens of agents eleven days - but the failures are. Every one stays on the screen. No concrete poured, no contract signed, no filing submitted, no materials wasted.

Code can fail before anyone relies on it

When I moved this website to a new platform, I did not check 100 web pages by hand. The agent built an evaluation gate that compared every page before and after the move, so a bulk change could not drop a paragraph without failing the build. For launch, it tested 146 redirects against the live site until every old link landed in the new location.

Speeding up a slow database query works the same way. The agent records what data is returned, rewrites the query, and checks the output is identical, only faster. It does not need to understand the user interface or the wider business. If you can say exactly what the output should be, it can grind until it matches.

Noah Smith quotes the investor Clifford Sosin on why this works: coding and maths "have relatively smooth solution spaces and are tractably verifiable". Then the sting: "Most of what matters doesn't behave like that."Ouch. For the record, I think coding and maths matter. Just not as much as emptying the bins, which no AI has offered to do yet.

Mathematicians rebuilt the work so a machine could check it

Maths was not always checkable by machine. Russell and Whitehead needed several hundred pages of Principia Mathematica before 1+1=2 could follow, a result most five-year-olds take on trust. When Thomas Hales proved the Kepler conjecture in 1998, twelve referees spent four years on it and declared themselves only 99% certain. They couldn’t check the computer calculations. So Hales set out to have a machine check every step. That took eleven years.

Lean changed the economics. Its creator, Leonardo de Moura, explains that a shared library of formal maths lets strangers fill gaps in each other’s work without having to trust each other. The kernel verifies every contribution. And once trust stops mattering, an AI is just another stranger. Scott Aaronson says maths fell first because it has “completely self-contained ways of checking that a solution is valid.” His physicist friends reckon they have six to twelve months.

So which profession goes next?

Aaronson noted that every field tells itself the ones already gone were trivial, and that it is safe. Law? Accounting? Pharmacy? Engineering? Each involves the physical world. Courts do not rerun a trial until you like the verdict. HMRC will not accept fifty versions of your year-end accounts. Drug trials need patients. And nobody pours a thousand concrete beams to see which ones crack.

But any profession is a bundle of tasks, and some of them already have a free retry. Put any task through two questions. Can it fail safely? Can a machine tell it failed? This month Mercor tested 12 licensed CPAs against AI on month-end close tasks. The accountants averaged about 37%. Claude Opus 5 scored 100% on all 20 attempts, each in under ten minutes. Read the setup, though, and you find a spherical horse in a vacuum: clean ledgers, complete documents, an answer known in advance. That is exactly the conditions that offer a free retry. A reconciliation can provide a clear check - the real month-end with the missing invoice and the client who hasn’t replied, does not.

Some engineering tasks already pass the first test. Finite element analysis replaced hand calculation decades ago, and a parametric model will size a thousand beams in an afternoon. Every one of those beams can fail safely, inside the software. The second question, how a machine tells a beam failed, is answered by the codes of practice. A Eurocode isn't a model of how a building behaves. It is a cautious envelope, agreed in advance: multiply every permanent load by 1.35 and check the result fits.I had originally written "every dead load by 1.4", like any engineer who grew up on British Standards would. When I was fact checking, according to Claude: "1.35 is the current figure, and any engineer under about 40 learned it first". Again, ouch. Codes of practice provide explicit checks for parts of the design. The harder question is how to check the work around those calculations: specification clauses, RFI responses and drawing notes.

Write down what correct looks like

The useful lesson from code and formal mathematics is the work done to make results checkable. Programmers write tests. Mathematicians express proofs in a form a machine can verify. Those checks give an AI agent a way to reject a failed attempt and try again.

Your firm may already have a starting point. Design codes, professional regulations and QA checklists specify parts of what good work requires. Some can become automated checks. Others still depend on information or judgement that the check cannot capture.

A firm that writes its rules as checks, not lore can put each new model to work against a clearer standard. But the check needs scrutiny too. An agent will pursue whatever it rewards, by whatever route it can find. You still set the standard, and your name still goes on the work.

Pick one process you run every week. Write down what a correct result looks like, precisely enough for a machine to check it. Then ask what you could retry a thousand times before lunch.