Josep Curto
Academic Director of the Master's Degree in Business Intelligence and Big Data at the Open University of Catalonia (UOC) and Adjunct Professor at IE Business School
When we read headlines about artificial intelligence (AI) systems "solving open mathematical problems that had been stalled for decades," it is easy to get swept up in the narrative of inevitable progress. However, a close examination of the technical details in the paper on AlphaProof Nexus—published in Science by researchers at Google DeepMind—reveals a pattern that has become all too common in the current AI landscape: a dazzling display of technical capability marred by significant methodological inconsistencies and a severe case of over-engineering.
The paper presents AlphaProof Nexus as an advanced framework for searching for formal proofs in Lean. The authors built a "complete" agent (Agent D) that combines a basic generate-verify loop, integration with the AlphaProof prover via reinforcement learning, and an evolutionary algorithm guided by a voting system and Elo ratings among sub-agents. On paper, the figures are impressive: the autonomous solution of nine open problems from the famous Erdős list, 44 OEIS conjectures, and applied discoveries in optimization and graph theory.
But when one delves deeper into the methodology and the study's own post hoc analysis, the conceptual structure begins to crack.
First. The authors' own ablation analysis reveals a damning fact: Agent A—a basic, simple "Ralph loop" alternating between LLM generation and Lean compiler verification—solved the same nine Erdős problems as the sophisticated Agent D. What does this tell us? That the framework's complexity is not what drives discovery; what really moves the needle is the base capability of the LLM (in this case, Gemini 3.1 Pro) combined with the direct, uncompromising feedback of the formal compiler.
Second. From a data and resource management perspective, the study’s financial assessment is, at best, opaque. Regarding inference cost metrics (in USD), the study shows that simplified agents are more cost-effective for most problems, whereas Agent D justifies its cost only in specific instances, such as Erdős #125. The article omits two relevant details: the calculations account only for inference during successful runs, and the reported costs for Agents B and D exclude the inference cost associated with AlphaProof.
Third, there is a misconception that using a formal language like Lean eliminates "hallucination." While Lean guarantees the logical validity of a proof relative to the statement written in Lean, it does not guarantee that said statement faithfully translates the actual mathematical problem. The article acknowledges several scenarios in which agents hallucinate or fall prey to errors in formalization. This demonstrates that the system still requires intensive expert human oversight to verify that what the agent has proven is indeed what was intended to be proven.
The true lesson of this work—even if the authors attempt to qualify it—is that both the market and the research community should lean toward simplicity: clean agentic loops, powerful language models, and environments with strict feedback mechanisms (compilers, code execution, unit tests, and expert human oversight)—though such setups are likely beyond the reach of many universities and research institutes. Everything else, for the time being, amounts to evolutionary fireworks that add architectural complexity rather than tangible results.