Researchers built an AI system that pairs language model reasoning with the Lean proof assistant, and it aced every olympiad math benchmark tested.
Magenta is a training-free, agentic pipeline: given only a natural-language math problem, it produces an answer, translates that answer into a Lean 4 statement, and then builds a machine-checked proof for it. Two internal judges keep the process honest. One checks that the Lean statement actually matches the original problem, so the system cannot quietly solve a different question and call it done. The other decides whether a failed attempt needs fresh mathematical re-derivation or just a local repair to the Lean proof. Running this loop, Magenta hit 100% accuracy across every olympiad benchmark tested, including AIME 2025, AIME 2026, and HMMT February 2026, and, paired with the open-weight K2-Horizon-7B model, solved all six problems from IMO 2026.
That statement-checking step is the real contribution. Language models are already decent at informal math reasoning, but decent is not the same as verified - a fluent-sounding proof can still be wrong. By forcing every answer through Lean and rejecting formalizations that drift from the original question, Magenta closes a gap that resampling and self-critique alone have not.
Still, a 100% score on graded competition problems with known answers is a controlled result, not proof this approach scales to open mathematical questions where nobody already knows the answer.