Primary evidence
- Magenta: Closing the Loop Between Mathematical Reasoning and Lean VerificationS1 · Primary research · Paper · 2026-09-10
Magenta closes the loop between informal mathematical reasoning and Lean verification
Magenta uses a statement judge to check whether a generated Lean statement preserves the original informal problem and an error-attribution judge to decide whether a failed attempt should return to mathematical re-derivation or local Lean repair.
What happened?
The Magenta paper introduced a training-free agentic pipeline that starts from a natural-language problem, derives an answer, formalizes the statement in Lean 4 and constructs a machine-checked proof; the authors report 100% accuracy on their evaluated Olympiad benchmarks and, with K2-Horizon-7B as the reasoner, successful proofs for all six IMO 2026 problems.
Magenta uses a statement judge to check whether a generated Lean statement preserves the original informal problem and an error-attribution judge to decide whether a failed attempt should return to mathematical re-derivation or local Lean repair. The paper reports that this feedback-guided correction loop outperforms independent resampling on difficult problems.
Why it matters
The work makes formal verification an active part of mathematical reasoning rather than only a final certificate. In particular, it addresses a central failure mode of end-to-end autoformalization systems: a prover can certify the wrong formal statement unless the pipeline also checks whether that statement faithfully represents the human problem.
Significance rationale: Magenta is a field-level milestone in verifier-guided mathematical agents because it integrates informal problem solving, Lean statement construction, statement-faithfulness judging, proof search and error attribution into one feedback loop instead of treating formalization and proving as isolated stages.
Historical context
Earlier developments
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Autonomous primary role
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Informal, Formal, Hybrid
- AI contribution
- Language-model agents perform the mathematical derivation, translate the result into Lean, construct proofs, judge statement fidelity and route failures between mathematical re-reasoning and Lean repair inside the evaluated pipeline.
- Human contribution
- Researchers designed the multi-stage pipeline, judges, routing logic and evaluation protocol, selected the underlying reasoners and benchmarks, and analyzed the failure and correction behavior.
- Verification
- Paper released · E2 · Research record · Machine-checked
- Last reviewed
- 2026-09-14
Technical details
- Systems
- magenta, lean, k2-horizon-7b
- Organizations
- —
- Problems
- olympiad-mathematics, imo-2026
- Methods
- agentic-theorem-proving, autoformalization, statement-verification, error-attribution, lean-feedback
Sources & artifacts
- Magenta: Closing the Loop Between Mathematical Reasoning and Lean VerificationS1 · Primary research · Paper · accessed 2026-09-14
Verification history
- 2026-09-10 · Paper released · E2 · Research record
The arXiv research record describes the Magenta pipeline and reports the benchmark and IMO 2026 results. The paper states that successful outputs are checked in Lean 4; no independent replay or public proof artifact is recorded by the Chronicle at this stage.
Corrections
No corrections recorded.