What we are reading

Verified is not finished

In September the mathematician Terence Tao spent twenty-five minutes arguing that his field has acquired a new kind of problem: results arriving faster than anyone can explain, review or absorb them. He calls the backlog proof indigestion. The subject is mathematics; the mechanism will be familiar to anyone who has watched automated output pile up faster than a team can take responsibility for it.

Two stages got faster. Four did not.

Tao breaks problem-solving in his field into six stages. Someone poses an open question. Someone proposes an answer. The answer gets checked. Then it has to be explained, because a first proof is often unreadable. Then accepted, meaning colleagues understand it too. Then absorbed: into textbooks, connected to everything else, taught to the next generation.

Machines have transformed stages two and three. Proposing and checking are fast now, and getting faster. Nothing downstream has moved. So the field is accumulating results that are correct, machine-checked, and that nobody has explained, while the last stage, the one that produces textbooks, is what generated the material that made the machines good at this in the first place.

His objection is not that the output is wrong. It is that correctness was never the only thing the process produced. A person who solves something hard can be asked how. They give talks, teach students, stay in the field for decades, and notice things along the way that become the next generation of open questions. A machine proof delivers the result and none of the rest.

“Almost anything that can be graded is useless.”

Terence Tao

The line is about optimisation targets. A target has to be checkable before you can optimise against it, and what is checkable and what is important are nearly disjoint sets, aligned only while you push gently. Push hard on any measurable proxy and you erode the thing it stood for. He is describing benchmark capture in a field with better ground truth than almost any other.

Why this reads differently outside mathematics

Our read, not his. If you deploy automated work anywhere a security review decides whether software ships, the shape is recognisable: output that passes every check, arrives faster than it used to, and has no author anyone can question. The reviewer's objection is rarely that a result is wrong. It is that nobody can say how it got there, what it was working to, or who accepted it.

Where the analogy stops. Tao is describing a scholarly commons with centuries of accumulated exposition at stake, and his prescription is to slow down; he says plainly there is no reason to move this fast. That is not a claim we are making. A regulated deployment is not a research field, the pressures are different, and going slower is rarely on offer to anyone with a delivery date. What travels is the narrower point: verification and accountability are two different problems, and solving the first does not touch the second.

One detail is worth sitting with. Across two of the open challenges his nonprofit ran this year, the winning entries barely used models at all. In one, the top team were two experts doing traditional computation. That is not an argument that the tools do not work. It is an argument about where judgement still sits.

This is our summary and our commentary. The views are the speaker's, and they have no association with Agentic Ensemble and have not reviewed or endorsed anything on this page. Watch the original; it is the better source.