aiqbench analysis
Magenta represents a significant advancement in AI by integrating formal verification tools like Lean 4 directly into the reasoning loop of large language models, effectively bridging informal natural language understanding with rigorous machine-checkable proofs. This training-free agentic pipeline demonstrates that combining LLMs with discrete mathematical verification can achieve perfect accuracy on high-difficulty benchmarks such as the IMO and AIME, addressing critical reliability issues in automated theorem proving. The work highlights a crucial shift from purely probabilistic reasoning to hybrid systems where error attribution and statement adjudication ensure robustness against hallucinations.
Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
arXiv:2609.11319v1 Announce Type: new 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.
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.
Artificial Intelligence (cs.AI)
arXiv:2609.11319 [cs.AI]
(or arXiv:2609.11319v1 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2609.11319 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 284 words
Related coverage
Verifying Rust cryptography in SymCrypt, from standards to code
Microsoft Research · Jul 13, 2026
[AINews] not much happened today
Latent Space · Sep 18, 2026
Lattice-Based Cryptography Explained
Quantum Zeitgeist · Aug 15, 2026
Links #3: 2026/06 Part 1
LessWrong · Jun 15, 2026