The Trace Is Not the Proof

Reasoning models now write out their steps. Checking those steps is a precise operation that exists for some problems and not for others, and the reliability of machine reasoning is set by that boundary rather than by the model.

Diogo Ribeiro — Faculdade de Media Artes e Design, Universidade Técnica do Porto. ORCID 0009–0001–2022–7072.

Two results from the same laboratory, five months apart, describe the whole problem.

In December 2025, Google DeepMind ran a mathematics agent built on Gemini Deep Think over the roughly 700 problems still marked open in Thomas Bloom’s database of Erdős problems. The agent, internally named Aletheia, generates a candidate solution in natural language, passes it to a verifier that is itself a language model, and revises on the verifier’s objections. Of 700 problems, 212 came back flagged as potentially correct. A team of human mathematicians then read them. Sixty-three were technically correct. Of those, fifty were, in the authors’ own phrase, technically valid but mathematically vacuous, because the problem statement had been read in a way Erdős did not intend and the resulting claim was easy. Thirteen addressed the problem as meant. Four of those were new.

In May 2026 the same laboratory reported AlphaProof Nexus, an agent in which language-model subagents search for proofs with feedback from the Lean…