Magenta links natural language math problems to verified formal proofs
Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
Artificial Intelligence
Summary
Solving math problems often involves informal explanations that humans understand but computers struggle to verify rigorously. The authors created Magenta, a system that starts with a math problem in plain English, rewrites it into a precise computer language called Lean, and then constructs a proof that a machine can check for correctness. Magenta also checks whether it translated the problem correctly and uses smart error correction to fix mistakes, achieving perfect accuracy on challenging math contests. This approach helps computers reliably handle math reasoning while still understanding natural language problems.
What this means in practice
- •For software developers: Build systems that can automatically generate verified code or proofs from natural language problem descriptions.
- •For automated testing teams: Use Magenta to create precise, machine-verified test cases from informal specifications to improve software reliability.
Authors
Joshua Ong Jun Leang, Haonan Li, Zheng Zhao, Xinyi Shang, Wenda Li, Zhengzhong Liu, Erix Xing, Shay Cohen, Eleonora Giunchiglia
Abstract
Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they achieve strong performance, yet not perfect, in informal mathematical reasoning. Restraining LLMs to informal reasoning misses out on the opportunity to use the discrete verification abilities that machines offer through machine-checkable proofs. In this paper, we bridge the gap between informal and formal reasoning by integrating Lean signals into the informal reasoning process. We introduce Magenta, a training-free agentic pipeline that, given only a natural-language problem, produces an answer, expresses it as a Lean 4 statement, and constructs a machine-checked proof. A statement judge verifies whether the formalisation preserves the original problem, while an error-attribution judge routes failed attempts either to mathematical re-derivation or local Lean repair. Magenta achieves 100% accuracy across all evaluated olympiad benchmarks, including AIME 2025, AIME 2026, and HMMT February 2026. When paired with the open-weight K2-Horizon-7B reasoner, it solves all six IMO 2026 problems. Our analysis shows that statement adjudication is essential for preventing false certificates and that feedback-guided correction outperforms independent resampling on difficult problems.