Magenta

A training-free agentic pipeline from MBZUAI's Institute of Foundation Models with Edinburgh and Imperial that feeds Lean 4 signals back into informal mathematical reasoning. Given a natural-language problem, Magenta produces an answer, expresses it as a Lean statement, and constructs a machine-checked proof; a statement judge checks that the formalisation preserves the problem and an error-attribution judge routes failures back to the reasoning. The headline is what it does for a small model: K2-Horizon-7B with Magenta reaches 100% on AIME 2025, AIME 2026, and HMMT February 2026 (from 74.19%) and solves all six IMO 2026 problems, which the paper presents as the smallest reasoner reported to do so, against 84.95% for the 375B K2 Horizon alone. No code release is linked.