A math AI that writes proofs all at once, not word by word, cracks a problem its rival missed

Most AI language models write like someone typing without a backspace key: one word at a time, left to right, each word locked in before the next. That's "auto-regressive" generation. It has a weakness for math proofs, which can run long: an early mistake gets baked in, and later steps drift out of sync with earlier ones. The model can't go back and fix what it already committed to.

This paper tries a different engine. A "diffusion" model starts with a rough, garbled draft of the whole proof and sharpens it over several passes — refining the entire block of text at once rather than crawling left to right. Because every pass can see the whole proof, both the parts before and after any given spot, the model keeps the late steps consistent with the early ones.

The team built two such 7-billion-parameter models. One writes complete proofs. The other is a fixer: it can blank out a broken chunk in the middle of a proof and rewrite it using context from both sides, like patching a sentence by reading the paragraph around the hole.

Against an ordinary word-by-word model trained on the same data, it scored 1.61 points higher on one proof benchmark and 6.14 higher on another. It also solved one International Math Olympiad problem a stronger rival model couldn't.

Those gains are modest, and they're measured against one matched baseline, not the whole field — this is a first proof of concept, not a finished champion.

Why you should care: Formal proofs are checked by computer, so they're either right or wrong — no partial credit, no bluffing. Showing that whole-proof revision beats one-word-at-a-time on these unforgiving tasks hints at where AI math reasoning could go next.