# Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

arXiv: https://arxiv.org/abs/2609.11319 · HTML: https://mlsanity.com/paper/2609.11319/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 21 of its 52 references that are in the map.
- First posted on arXiv 10 Sep 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 21 of 21)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [OpenAI GPT-5 System Card](https://mlsanity.com/paper/2601.03267/) (2025)
- [Skywork-Reward: Bag of Tricks for Reward Modeling in LLMs](https://mlsanity.com/paper/2410.18451/) (2024)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [A Survey on Test-Time Scaling in Large Language Models: What, How, Where, and How Well?](https://mlsanity.com/paper/2503.24235/) (2025)
- [Kimi K3: Open Frontier Intelligence](https://mlsanity.com/paper/2607.24653/) (2026)
- [Big-Math: A Large-Scale, High-Quality Math Dataset for Reinforcement Learning in Language Models](https://mlsanity.com/paper/2502.17387/) (2025)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)
- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning](https://mlsanity.com/paper/2603.21065/) (2026)
- [OProver: A Unified Framework for Agentic Formal Theorem Proving](https://mlsanity.com/paper/2605.17283/) (2026)
- [Moonshine: An Autonomous Mathematical Research Agent Centered on Conjecture Generation](https://mlsanity.com/paper/2606.10806/) (2026)
- [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](https://mlsanity.com/paper/2608.10916/) (2026)
- [Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation](https://mlsanity.com/paper/2606.12594/) (2026)
- [Rethinking Math Reasoning Evaluation: A Robust LLM-as-a-Judge Framework Beyond Symbolic Rigidity](https://mlsanity.com/paper/2604.22597/) (2026)
- [Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning](https://mlsanity.com/paper/2605.28365/) (2026)
- [Evaluation of LLMs for Mathematical Formalization in Lean](https://mlsanity.com/paper/2606.05632/) (2026)
- [Pipeline for Verifying LLM-Generated Mathematical Solutions](https://mlsanity.com/paper/2602.20770/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language](https://mlsanity.com/paper/2607.16372/) (2026)

## Built on by (most cited first, 1 of 1)

- [Euler: Towards Human-Centered Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2610.19864/) (2026)

## Abstract (arXiv)

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.