Summary (Overview)

• MAGENTA is a training-free agentic pipeline that bridges informal mathematical reasoning (via LLMs) and formal verification (via Lean 4), given only a natural-language problem.
• It produces three outputs: an informal reasoning chain, a candidate answer, a Lean 4 statement, and a machine-checked proof, all through verification-guided self-correction.
• The pipeline introduces a statement judge to ensure the formal statement faithfully represents the original problem, and an error judge that attributes verification failures to either mathematical (MATH) or syntactic (SYNTAX) causes, routing feedback accordingly.
• MAGENTA achieves 100% verified accuracy on AIME 2025, AIME 2026, and HMMT February 2026 (93 problems total), with gains of 8.6–25.8 percentage points over standalone reasoners.
• The system is robust to paraphrasing, does not rely on closed-source models for the core loop, and demonstrates that verification-guided self-correction outperforms naive resampling, especially on harder problems like IMO 2026.

---

Introduction and Theoretical Foundation

Background and Motivation

• Mathematical knowledge is predominantly communicated through informal natural language, which LLMs handle well but not perfectly.
• Chain-of-thought (CoT) reasoning and test-time scaling have improved LLM performance on competition mathematics, yet longer reasoning traces still contain errors and dead ends.
• Existing supervision signals (LLM judges, process reward models) are learned proxies for correctness—they reproduce the failure modes of the models they evaluate and score plausible-but-incorrect reasoning.
• Formal verification (e.g., Lean 4) offers a deterministic, machine-checkable correctness signal, but prior systems (e.g., DeepSeek-Prover, InternLM) assume a formal goal is already available, ignoring the central challenge of autoformalisation: determining precisely what a natural-language problem asks to prove.

Theoretical Foundation

The paper formalises the pipeline over the following spaces:

• $\mathcal{Q}$: space of natural-language mathematics problems
• $\mathcal{C}$: space of informal reasoning chains
• $\mathcal{A}$: space of candidate answers
• $\mathcal{S}$: space of Lean 4 theorem statements
• $\mathcal{P}$: space of Lean 4 proof scripts
• $\mathcal{E}_p$: Lean diagnostics from failed proof verification
• $\mathcal{E}_s$: Lean diagnostics from failed statement elaboration
• $\mathcal{F}_{\text{math}}$: mathematical correction feedback signals

Key formal operations include:

• Formaliser: $s \sim F(q, a)$ — samples a Lean statement from problem and answer.
• Verifier (statement): $V_s(s)$ — checks that the statement elaborates and is closed (well-formedness only).
• Verifier (proof): $V_p(s, \pi)$ — checks that proof $\pi$ is a valid proof of statement $s$.
• Statement Judge: $J_s(q, a, s)$ — adjudicates whether $s$ faithfully represents $q$ and $a$.
• Error Judge: $J_e(q, c, a, s, \pi, \text{diag}) \rightarrow \{\text{MATH}, \text{SYNTAX}\}$ — attributes verification failure.

The paper also sketches a mistake-bound model for analysing the pipeline's convergence, where the number of mistakes per problem is bounded, and discusses conditions under which the closed-loop pipeline provably terminates with a verified certificate.

---

Methodology

Pipeline Overview

MAGENTA operates as an iterative, verification-guided refinement loop:

1. Reasoner: Given problem $q$, generates informal reasoning chain $c$ and candidate answer $a$.
2. Formaliser: Converts $(q, a)$ into a Lean 4 statement $s \sim F(q, a)$.
3. Statement Judge: Checks alignment between $s$ and $(q, a)$. If misaligned, resamples the formalisation.
4. Prover: Uses informal reasoning $c$ as a proof plan to generate Lean proof $\pi$.
5. Verifier: Checks $V_p(s, \pi)$. If verification fails:
   • Error Judge labels the failure as SYNTAX or MATH.
   • SYNTAX: local proof regeneration (fix Lean implementation, keep mathematical content fixed).
   • MATH: feedback $\varphi \in \mathcal{F}_{\text{math}}$ is returned to the reasoner for mathematical re-derivation.

Key Design Choices

• Statement Judge prevents false certificates: since Lean verifies a proof only relative to the generated statement, $V_p(s, \pi) = \top$ does not imply $s$ faithfully represents $q$. The judge works under the assumption that confirming alignment is easier than generating the formal statement.
• Error Judge resolves the underdetermination of a failed verification: without it, the pipeline has no basis to choose between proof repair and mathematical re-derivation.
• Training-free: A single language model, prompted in two distinct ways, implements the two judging functions; no fine-tuning is required.
• Backends: Open-weight models (e.g., K2-HORIZON-7B/375B, Qwen3.8-27B) as reasoners; formaliser/prover can be specialised open-source models or closed-source (e.g., GPT-5.6-Sol/Codex).

Algorithm Summary

The pseudocode (Appendix A.2) describes the iterative loop: reason → formalise → adjudicate → prove → verify → attribute → repair. The loop continues until either a verified and adjudicated certificate is produced, or the budget (number of rounds) is exhausted.

---

Empirical Validation / Results

Experimental Setup

• Benchmarks: AIME 2025, AIME 2026, HMMT February 2026 (93 problems total, all with numerical answers and no accompanying formal statements).
• Baselines: Standalone reasoners (K2-HORIZON-375B, K2-HORIZON-7B, Qwen3.8-27B) at pass@1.
• Paraphrase control: AIME 2026 problems are paraphrased using DeepSeek-V4-Flash, checked with CODEX, to measure the robustness gap $\Delta$ against data contamination.

Key Results

Table 1: Accuracy (%) on competition-level mathematics benchmarks

• MAGENTA achieves 100% verified accuracy across all three benchmarks with all reasoners.
• Replacing the formaliser/prover with GPT-5.6-Sol (Codex) also yields perfect scores, showing backend flexibility.

Robustness to Paraphrasing

Table 2: Accuracy (%) on original and paraphrased AIME 2026

• MAGENTA shows zero robustness gap ($\Delta = 0$), whereas standalone reasoners lose 3.3–10.0 points under paraphrasing.
• This is necessary (though not sufficient) evidence against contamination.

Self-Correction Dynamics

• On IMO 2026, self-correction verifies all 6 problems, while naive resampling (8–16 independent generations) verifies only 1/6 (16.7%).
• The 7B reasoner closes the gap to 100% by spending additional verification-guided correction rounds, while the 375B model converges faster.
• Ablation: Removing the statement judge causes VerCor (verified correctness) to fall 43.3 points to 20.0% and the false-certificate rate (FCR) to rise to 45.5%—nearly half of surviving certificates prove something other than the problem asked.
• Ablation: Removing the error judge (i.e., naive resampling) fails to reach verified proofs on most IMO problems, showing that diagnostic-conditioned correction moves probability mass onto proofs the unconditioned distribution does not reach.

Residual Gap

• Despite perfect verified accuracy, a residual gap remains between the informal explanation and the formal statement/proof. A final alignment judge (K2-HORIZON-375B) returns "incomplete proof" when the two do not support the same conclusion.
• Formal correctness is attainable with a compact reasoner, but a fully aligned, communicable informal derivation remains a separate challenge.

---

Theoretical and Practical Implications

Theoretical Implications

• Error attribution matters: The paper provides empirical evidence that conditioning on a diagnostic (MATH vs. SYNTAX) is essential for convergence; without it, resampling under the same budget fails on hard problems.
• Mistake-bound model: The paper sketches a learning-theoretic analysis (mistake-bound framework) for the pipeline, suggesting that the number of external feedback rounds per problem is bounded, though exact values of $\gamma$ or $M(q)$ are difficult to pin down given LLM inference complexity.
• Formalisation gap: The central theoretical limitation is the autoformalisation gap—verification guarantees correctness only relative to the generated statement, not unconditionally with respect to the original problem. Closing this gap is a question of better autoformalisation, not better proof search.

Practical Implications

• Training-free and model-agnostic: MAGENTA works with open-weight reasoners (7B–375B) and both open and closed formaliser/prover backends, making it accessible and cost-controllable.
• Cost analysis: At equal verified accuracy, MAGENTA moves cost from metered external rounds into local computation one controls (e.g., a CODEX CLI call reports one call regardless of internal compiler queries, while LEANSTRAL multi-turn agents may hide hundreds).
• Reliability: MAGENTA is robust to paraphrasing, addressing contamination concerns and demonstrating that verification-guided correction is more reliable than raw resampling.
• Certificates: The pipeline produces machine-checkable certificates, meaningful only when the statement judge confirms alignment with the original problem.

---

Conclusion

MAGENTA introduces a training-free agentic pipeline that couples informal mathematical reasoning with Lean 4 formal verification. Given only a natural-language problem, it produces a reasoning chain, candidate answer, formalised Lean statement, and machine-checked proof, guided by two judges: a statement judge for formal–informal alignment and an error judge for attributing verification failures to mathematical or syntactic causes.

Key takeaways:

• Perfect verified accuracy (100%) on AIME 2025, AIME 2026, and HMMT February 2026.
• Robustness to paraphrasing ($\Delta = 0$), unlike standalone reasoners.
• Diagnostic-conditioned self-correction outperforms naive resampling, especially on IMO 2026.
• The main remaining obstacle is autoformalisation: ensuring the generated Lean statement faithfully represents the original problem.

Future directions include improving autoformalisation quality, extending the mistake-bound analysis, and scaling the pipeline to more diverse mathematical domains.