Preprint: Magenta reportedly turns olympiad math into Lean statements and machine-checked proofs

A new arXiv preprint says researchers have built an AI system that can take olympiad-style math problems written in ordinary language, convert them into the Lean proof assistant, and produce machine-checked proofs. In the paper, the authors report perfect verified results on recent benchmark sets and say that, when the system was paired with the open-weight K2-Horizon-7B model, it “solves all six IMO 2026 problems.”

The result, if it holds up, would mark a notable step in AI math and formal verification. But the claim is so far limited to a research preprint. The paper, posted to arXiv on Sept. 10 as arXiv:2609.11319v1, does not link a public code repository, and no public release of the generated Lean theorem files or proofs was found at the time of review. The results also have not been independently reproduced here.

The paper, “Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification,” is led by Joshua Ong Jun Leang and includes researchers affiliated with the Institute of Foundation Models at MBZUAI, Imperial College London, the University of Edinburgh and University College London. In the abstract, the authors write: “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.”

In plain terms, Magenta is meant to close a hard gap in automated mathematics. A proof assistant such as Lean can verify that a formal proof is logically valid, but it does not by itself ensure that the formal statement exactly matches the original problem as written in natural language. The paper says Magenta addresses that with two checks: a “statement judge” that evaluates whether the Lean formalization matches the original problem, and an “error-attribution judge” that decides whether a failed attempt reflects a math error or a Lean implementation issue, then routes the system toward either re-deriving the solution or repairing the proof locally.

The benchmark numbers reported in the paper are striking. According to Table 1, the system reached 100% verified accuracy on AIME 2025, AIME 2026 and HMMT February 2026, covering 93 olympiad-style problems in total. The paper’s headline claim goes further: “When paired with the open-weight K2-Horizon-7B reasoner, it solves all six IMO 2026 problems.” K2-Horizon-7B is publicly available as an open-weight model through IFM on Hugging Face.

The authors say they counted a solution as complete only if it passed Lean 4.29.1, SafeVerify and an additional check comparing the informal reasoning with the formal certificate. For the IMO 2026 results, the paper says evaluation used automatic scoring with CODEX as well as independent marking by what it describes as “a former IMO medallist.”

That distinction between informal math and formal proof is why the claim matters. Over the past two years, systems such as AlphaProof and AlphaGeometry, along with other verifier-based pipelines, have shown increasingly strong olympiad-level performance. But many earlier setups started from a problem that had already been formalized by humans. Magenta’s main claim is an end-to-end system: natural-language problem in, formal statement and machine-checked proof out.

That also points to the main reason for caution. Formal verification can certify a proof of a formal theorem, but outside researchers still need to inspect whether the formal theorem truly matches the original question and whether the reported pipeline works as described across the full benchmark. Without public code, generated Lean files or independent replication, the Magenta results remain author-reported preprint claims — notable ones, but not yet externally validated.