Found first: a primary source the press has not covered yet.
Meta FAIR researchers show that a minimal agentic harness with an efficient Lean 4 interface, called h1, outperforms DeepMind's specialized AlphaProof Nexus on open Erdős problems while costing less. The paper, posted to arXiv on October 25, 2026, argues this extends the bitter lesson in machine learning to formal theorem proving.
What the source says
The authors are Skander Moalla (FAIR / EPFL), Ahmad Rammal (FAIR / CERMICS-ENPC), Niket Patel (FAIR / NYU), Rémi Munos (FAIR), and Julia Kempe (FAIR / NYU). h1 gives a frontier model an efficient Lean 4 interface with verifier feedback and self-reflection, imposing no decomposition or search structure. On five open Erdős problems, h1 with Gemini 3.1 Pro achieves 82.5% pass@1 success at a mean cost of $121, versus AlphaProof Nexus basic at 75.4% for three attempts at $191 and full AlphaProof Nexus at 76% for $317. GPT-5.5 via h1 scores 670/672 on PutnamBench; GPT-5.6 Sol scores 90/100 on FATE-X, 78/100 on FormalConjectures100-Solved, and solves all 6 IMO 2026 problems. h1 settles 8 open FormalConjectures problems, including variants of Erdős 138 and 337.
Why it matters
Formal theorem proving has been treated as a domain that resists simple scaling: the search space is vast, proofs need structure, and specialized planning workflows seemed necessary. h1 contradicts that. A frontier model with only efficient Lean 4 feedback, run as a single attempt, Pareto-dominates full AlphaProof Nexus on the Erdős benchmark: higher success rate at lower cost. The authors conclude that efficient execution feedback largely determines solve rate and cost, and recommend evaluating frontier models with good tool interfaces before attributing any system's performance to its workflow design.