PaperlayerView exact revision on arXiv

Source-linked AI summary

Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

Joshua Ong Jun Leang, Haonan Li, Zheng Zhao, Xinyi Shang, Wenda Li, Zhengzhong Liu, Erix Xing, Shay Cohen, Eleonora Giunchiglia

arXiv:2609.11319v1cs.AI

TL;DR

MAGENTA addresses the gap between informal mathematical reasoning and machine-checkable formal proofs by integrating Lean verification into an agentic pipeline. It generates and adjudicates Lean statements, attributes failures to mathematics or implementation, and reports perfect results across evaluated olympiad benchmarks, including all six IMO 2026 problems with K2-HORIZON-7B.

  • Problem

    Existing informal reasoning can be incorrect, while formal-proving benchmarks commonly assume an accurate formal statement and therefore leave the informal-to-formal gap insufficiently addressed.

  • Method

    MAGENTA is a training-free pipeline that generates an answer and Lean 4 formalisation, uses a statement judge for semantic fidelity, and routes failed proofs through mathematical re-derivation or local repair.

  • Results

    MAGENTA verifies every problem across AIME 2025, AIME 2026, and HMMT February 2026, and K2-HORIZON-7B solves all six IMO 2026 problems.

  • Takeaways & Limitations

    Statement adjudication keeps certificates meaningful, while feedback-guided correction reaches proofs that independent resampling does not.

  • Takeaways & Limitations

    The certificate is formally sound with respect to the generated statement, but its relevance to the original problem depends on the learned judge’s semantic fidelity.

Abstract

from arXiv · show

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.

1 INTRODUCTION

MAGENTA integrates informal mathematical reasoning with Lean verification, addressing the gap between generating answers and guaranteeing that formal proofs represent the original problems. Its training-free pipeline uses adjudication and error-directed correction to produce verified solutions.

  • 1 INTRODUCTION: Existing formal-proving benchmarks typically provide human-written formal statements, leaving the autoformalisation problem largely unaddressed.Lean certificates guarantee proofs of stated theorems, but not that those theorems faithfully encode the original natural-language problem.
  • 1 INTRODUCTION: The pipeline explicitly separates statement rejection and proof-failure handling, resampling formal statements while routing mathematical and Lean errors differently.This design motivates evaluations of robustness, correction budgets, and ablations of the two mechanisms distinguishing MAGENTA from simple retries.
  • 1 INTRODUCTION: MAGENTA verifies every problem across AIME 2025, AIME 2026, and HMMT February 2026 with four reasoners, and solves all six IMO 2026 problems with K2-HORIZON-7B.The authors also report robustness to answer-preserving paraphrases and verification-guided self-correction beyond one-shot recall.
  • 1 INTRODUCTION: MAGENTA bridges informal reasoning and formal verification by producing an answer, Lean 4 statement, and machine-checked proof from a natural-language problem.A statement judge checks semantic fidelity, while failed attempts are routed for mathematical re-derivation or local Lean repair.

2 METHODOLOGY

MAGENTA combines language-model components with deterministic Lean checks in an iterative procedure that generates, adjudicates, proves, and repairs formal solutions. Its learned statement judge addresses the autoformalisation gap, while error attribution determines whether to revise mathematics or proof implementation.

  • 2.1 COMPONENTS: The reasoner samples informal chains and answers, the formaliser generates Lean statements conditioned on those answers, and the prover constructs scripts for accepted statements.The verifier is deterministic, while the reasoner, formaliser, prover, and judges are language-model components.
  • 2 METHODOLOGY: MAGENTA iteratively converts a problem and candidate answer into an adjudicated Lean statement, then uses verification feedback to refine the solution.The pipeline distinguishes mathematical reasoning from formal implementation so that only the responsible component is revised.
  • 2.2 THE MAGENTA PROCEDURE: After proof failure, the error judge labels the attempt MATH or SYNTAX, sending mathematical errors back for re-derivation and syntax errors to local proof regeneration.Successful Lean verification terminates the pipeline with the accepted statement, answer, reasoning chain, and proof.
  • 2.2 THE MAGENTA PROCEDURE: Statement adjudication accepts only formal statements that faithfully represent the original problem and candidate answer; rejected statements are resampled without changing the reasoning pair.A candidate must first elaborate in Lean before semantic adjudication and proof generation.
  • 2.3 ROLE OF THE JUDGE AND SCOPE OF THE GUARANTEE: Lean proves only the generated statement, so statement adjudication prevents formally valid certificates that are irrelevant to the original problem.Because semantic alignment is judged by a learned model rather than the Lean kernel, the final certificate is formally sound relative to the statement but only conditionally relevant to the question.

3 EXPERIMENTS

MAGENTA improves verified mathematical performance across multiple reasoners and configurations, including perfect results on the evaluated competition benchmarks and all six IMO 2026 problems with K2-HORIZON-7B. The experiments show that verification-guided correction trades additional computation for smaller model scale, while formal correctness does not ensure a fully aligned explanation.

  • 3 EXPERIMENTS: The evaluation uses competition problems without accompanying formal statements and compares MAGENTA with one-answer baseline generation.The benchmark set covers 93 problems in total, according to the Table 1 caption.
  • 3 EXPERIMENTS: MAGENTA verifies every problem on AIME 2025, AIME 2026, and HMMT February 2026 across four reasoners, with perfect scores also obtained using alternative formaliser and prover configurations.Average gains over standalone reasoners range from 8.6 points for Qwen3.8-27B to 25.8 points for K2-HORIZON-7B.
  • 3 EXPERIMENTS: The reported gains are not tied to a particular reasoner, formaliser, or prover configuration, suggesting that the verification-guided pipeline contributes beyond any single model.The authors note that replacing both formaliser and prover with GPT-5.6-Sol again yields perfect scores.
  • 3 EXPERIMENTS: K2-HORIZON-7B paired with MAGENTA solves all six IMO 2026 problems, while the authors identify a remaining gap between formal correctness and fully aligned, communicable informal derivations.A final alignment judge is added to flag cases where the informal explanation and formal proof do not support the same conclusion.
  • 3 EXPERIMENTS: Verification-guided correction trades test-time computation for model scale: K2-HORIZON-7B needs an average of 5 rounds on AIME 2026 versus 2 for K2-HORIZON-375B, with both reaching perfect accuracy.On IMO 2026, K2-HORIZON-7B requires an average of 5.7 mathematical-error correction rounds.

4 ANALYSIS

The analysis examines how formaliser choice, proof-backend accounting, paraphrase robustness, and judge ablations affect MAGENTA’s coverage, cost, and correctness. Feedback-guided correction and statement adjudication provide the clearest gains over independent resampling and unchecked formalisation.

  • FORMAL STATEMENT GENERATION: CODEX succeeds on the first formaliser call for approximately 66% of AIME 2026 problems versus 42% for Goedel and covers the benchmark within 6 rather than approximately 120 calls.At a six-call budget, Goedel covers only about 68%; an exhausted statement budget forfeits otherwise recoverable problems.
  • FORMAL PROOF GENERATION: Counting LEANSTRAL’s internal work reverses the external-cost ordering, with approximately 3 × 10^2 internal calls at median coverage and up to 3 × 10^3 at full coverage.The comparison therefore concerns moving cost from metered rounds into locally controlled computation, while CODEX’s hidden internal work makes its external measurements lower bounds.
  • FORMAL PROOF GENERATION: 100% of AIME 2026 is verified by both proof backends, while LEANSTRAL is left-shifted on external cost measures despite equal final coverage.LEANSTRAL reaches 42% with no failed external verification round versus 17% for CODEX, full coverage at approximately 6 × 10^4 versus 9 × 10^5 reasoner tokens, and proofs of 1.1 × 10^4 versus 2 × 10^4 tokens.
  • ROBUSTNESS TO ANSWER-PRESERVING PARAPHRASE: Paraphrasing costs K2-HORIZON-375B 3.3 points and K2-HORIZON-7B 10.0 points, whereas both retain 100% with MAGENTA (∆ = 0).The authors treat this answer-preserving paraphrase test as necessary rather than sufficient evidence against contamination.
  • ABLATION STUDY: Without statement adjudication, verified coverage falls from 63.3% to 36.7%, verified-correct coverage falls 43.3 points to 20.0%, and FCR rises to 45.5%.Every first-sampled formalisation is accepted in the ablation, showing that unchecked acceptance can preserve certificates for statements other than the requested problem.
  • ABLATION STUDY: Independent resampling solves 29/30 AIME 2026 problems (96.7%) versus 30/30 for self-correction, but on IMO 2026 it verifies only 1/6 (16.7%) versus all six.Diagnostic-conditioned correction routes subsequent attempts according to whether the failure is mathematical or syntactic.

5 RELATED WORK

Related work spans informal mathematical reasoning, formal theorem proving, and efforts to connect natural-language reasoning with formal proof. These lines of work motivate MAGENTA’s integration of learned reasoning signals with machine verification.

  • LLMs for Mathematical Reasoning: Competition-mathematics systems use chain-of-thought, test-time scaling, judges, process reward models, and related selection signals, but plausible reasoning can remain incorrect.
  • Theorem Proving and Autoformalisation: LLM theorem proving has advanced through specialised proving models and agentic closed-source systems, often with substantial test-time scaling.
  • Formal–Informal Distillation: Formal–informal distillation has explored links between natural-language reasoning and formal proof, but prior approaches often rely on closed models or underperform state-of-the-art mathematical reasoners.Other curated pipelines improve reliability, while theorem-prover-as-judge approaches use formal verification signals.

6 CONCLUSION

MAGENTA couples informal mathematical reasoning to Lean formalisation and machine-checked proof, using judges to route failures and preserve statement fidelity. The paper concludes that verification is relative to the generated formalisation, making better autoformalisation the main remaining obstacle.

  • 6 CONCLUSION: MAGENTA generates a reasoning chain, answer, Lean 4 statement, and checked proof, while statement and error judges route failures to formalisation, repair, or mathematical re-derivation.Accepted statements remain fixed during proof search; syntax failures trigger local repair, whereas mathematical failures return feedback to the reasoner.
  • 6 CONCLUSION: Verification guarantees correctness only relative to the generated formalisation, so closing the gap to the original problem requires better autoformalisation rather than better proof search.This scope boundary is identified as the main remaining obstacle to Lean-guided natural-language reasoning.
  • 6 CONCLUSION: The pipeline returns a verified tuple (c, a, s, π) or UNCERTIFIED after bounded reasoner, formaliser, and prover attempts.The controller uses budgets T, M, and K for reasoner attempts, statement samples, and proof attempts.
  • 6 CONCLUSION: A final completeness judge for IMO 2026 checks that the formal certificate covers and aligns with the informal solution after Lean certification.This filter adds an acceptance check without replacing Lean or changing feedback routing.

B IMPLEMENTATION DETAILS FOR MAGENTA

The implementation specifies prompt roles for solving, formalising, judging, proving, and classifying failures, while preserving the supplied theorem target and mathematical solution. Experiments use fixed inference budgets, Lean/SafeVerify certification, and distinct reasoner, judge, proof-agent, and comparator configurations.

  • B IMPLEMENTATION DETAILS FOR MAGENTA: The pipeline separates statement alignment from proof generation: judges assess fidelity, while proof agents repair Lean implementation without changing the immutable target.The prompts explicitly distinguish formal translation from independent mathematics and local implementation repair from mathematical correction.
  • B IMPLEMENTATION DETAILS FOR MAGENTA: The Lean proof prompt requires preserving the theorem signature and formalising the supplied mathematical solution without silently changing its assumptions, conclusion, or strategy.It prohibits fabricated assumptions, unsafe shortcuts, and unsupported exhaustive computation, and requires iterative Lean-based repair.
  • B IMPLEMENTATION DETAILS FOR MAGENTA: Failures are classified as code_error unless verifier evidence exposes false or insufficient mathematics; ambiguous cases are routed as code_error.Code errors include syntax, elaboration, typing, tactic, timeout, protocol, and incomplete-proof failures that preserve the mathematics.
  • B IMPLEMENTATION DETAILS FOR MAGENTA: Experiments use T = 32 reasoner attempts, M = 512 formal-statement samples, and K = 4096 proof attempts per accepted statement.The main reasoner uses temperature 0.6, top p = 0.95, and maximum outputs of 64,000 tokens, or 128,000 for IMO 2026.
  • B IMPLEMENTATION DETAILS FOR MAGENTA: Final certification requires an unchanged theorem statement, zero exit codes from Lean and SafeVerify, no timeouts, and no forbidden constructs.The proof environment uses Lean v4.29.1 and rejects sorry, admit, new axioms, unsafe declarations, and native_decide.

C REFINEMENT ROUNDS ACROSS MODELS AND DATASETS

Refinement effort differs substantially by reasoner and dataset: K2-Horizon-7B needs more rounds on harder benchmarks, whereas K2-Horizon-375B usually succeeds near its initial attempt. The section also includes examples of corrected reasoning and verified counting proofs.

  • C REFINEMENT ROUNDS ACROSS MODELS AND DATASETS: K2-Horizon-7B averages approximately 1, 2, and 3 refinement rounds on AIME2025, AIME2026, and HMMT2026, with maxima of 3, 5, and 10.K2-Horizon-375B averages approximately one round across all three datasets, with at most one additional round on AIME2026 and HMMT2026.
  • C REFINEMENT ROUNDS ACROSS MODELS AND DATASETS: The shorter K2-Horizon-375B trajectories are consistent with its reported tendency to produce correct answers on the first attempt.For K2-Horizon-7B, increasing refinement effort suggests greater difficulty on AIME2026 and HMMT2026, although the relationship requires further assessment.
  • C REFINEMENT ROUNDS ACROSS MODELS AND DATASETS: An audited AIME 2026 trajectory recovers from an initially wrong informal solution after the error is attributed to mathematics rather than Lean implementation.The failed cycle occupies boxes 1–5 and the corrected cycle boxes 6–9.
  • C REFINEMENT ROUNDS ACROSS MODELS AND DATASETS: 1 permutation of six elements satisfies π^7 = id, because its order divides 7 but cannot equal 7 on a six-element set.The formal statement and proof identify the identity permutation as the sole solution.
  • C REFINEMENT ROUNDS ACROSS MODELS AND DATASETS: 396 permutations of six elements satisfy π^6 = id, obtained by counting the allowed cycle types whose lengths lie in {1, 2, 3, 6}.The cycle-type counts sum to 396, and the corresponding Lean theorem states the same cardinality.

E.1 FORMAL STATEMENT ERROR ANALYSIS

Formal-statement failures arise mainly from Lean elaboration and semantic misalignment rather than surface syntax. Semantic adjudication rejects many compilable statements, including weakened or answer-baked surrogate goals.

  • E.1 FORMAL STATEMENT ERROR ANALYSIS: Type, coercion, and projection mismatches account for more than half of rejected statements, while typeclass synthesis contributes almost a quarter.Together these categories explain over three quarters of pre-proof rejection; syntax errors are much less common.
  • E.1 FORMAL STATEMENT ERROR ANALYSIS: 67.08% of Lean-passing statements are rejected by the DeepSeek semantic judge, while 32.92% are accepted.Across all generated statements, these outcomes correspond to 44.64% rejected and 21.91% accepted.
  • E.1 FORMAL STATEMENT ERROR ANALYSIS: In the no-Js ablation, three of five falsely certified statements prove weakened or answer-baked surrogate goals.The remaining false certificates respectively drop an essential problem component or mistranslate the underlying geometry.
  • E.1 FORMAL STATEMENT ERROR ANALYSIS: Compilation is a weak proxy for faithfulness because semantic adjudication removes substantially more compilable-but-misaligned statements than Lean removes malformed ones.This establishes semantic alignment as a separate bottleneck from elaboration.

E.2 PROOF ERROR ANALYSIS

Proof failures occur at distinct internal and external levels, with debugging profiles differing between LEANSTRAL and CODEX.

  • Internal and external proof failures: 54.73% of LEANSTRAL’s de-duplicated internal Lean/LSP results contain an error diagnostic or tool failure.These include tactic, API, protocol, syntax, typing, and resource-limit failures.
  • Internal and external proof failures: External LEANSTRAL failures concentrate on unsolved proof obligations and SafeVerify policy violations.
  • Internal and external proof failures: CODEX’s external failures are dominated by type and coercion mismatches, followed by tactic failures and API misuse.Parser errors are negligible for both systems.
  • Internal and external proof failures: LEANSTRAL resolves a broader range of implementation errors internally, whereas CODEX exposes more of them externally.

E.3 REASONER ERROR ANALYSIS

The reasoner-error analysis attributes 14 AIME 2026 failures to preserving the problem statement and justifying key proof steps, motivating an additional completeness check.

  • Root causes and completeness: 14 mathematical errors were attributed to K2-HORIZON-7B by the error judge on AIME 2026.
  • Root causes and completeness: The dominant errors involve altered numbers or parameters, misread values or iteration counts, and unsupported geometric or combinatorial reductions.Examples include changing 17017 to 107017 and solving for N = 1000 instead of N = 10000.
  • Root causes and completeness: Compiler feedback alone is insufficient for these errors because some failures require reconstructing the mathematics rather than repairing Lean code.
  • Root causes and completeness: For IMO 2026, a final judge checks whether the formal certificate covers the complete informal solution before a solution is counted as complete.

F.2 EVALUATION

IMO 2026 solutions were assessed by automated and human marking, while token usage varied with problem difficulty under verification-guided self-correction.

  • Evaluation: IMO 2026 solutions were evaluated both by CODEX against reference solutions and independently by a former IMO medallist.
  • Evaluation: MAGENTA allocates more inference-time computation to harder IMO problems, with Problems 3 and 6 using the largest token budgets.These problems also require more self-correction.
  • Evaluation: Formal-verification feedback guides subsequent attempts, allowing the reasoner to revise unsuccessful arguments and allocate computation where needed.

F.4.1 IMO PROBLEM 1

The first IMO problem’s process terminates with exactly one number greater than 1, and that final value is independent of the choices made; the supplied passages also include a separate geometric argument.

  • Number process: A lexicographically decreasing pair (N, P) proves that the number process terminates after finitely many moves.N counts entries greater than 1, while P decreases whenever N remains unchanged.
  • Number process: The terminal board contains exactly one integer M > 1 and 2025 entries equal to 1.
  • Number process: The value M is independent of all choices because the p-adic valuation gcd invariant determines every vp(M) from the initial board.
  • Geometric argument: The geometric argument uses coordinates, determinant and dot-product angle identities, and positivity conditions to establish the requested circumcentre relation.The stated conclusion is OM = ON.
  • Additional argument: A separate cutting argument reduces the final alternating sum to the length r of one unmatched interval and bounds it by δ.

F.4.4 IMO PROBLEM 4

The problem asks when Mulan can force a finite victory in a triangle-cutting game where Shan-Yu discards one resulting triangle. The solution proves that this is possible exactly when θ divides 180°.

  • Problem setup: The game asks for all real θ with 0° < θ < 180° for which Mulan can guarantee victory regardless of Shan-Yu’s choices.A cut divides the current triangle into two triangles, after which Shan-Yu discards one.
  • Necessity: If θ does not divide 180°, Shan-Yu can prevent victory by discarding any triangle containing an angle that is an integer multiple of θ.The key lemma shows that each cut produces at most one such triangle, so an initial triangle without a multiple of θ can be maintained indefinitely.
  • Sufficiency: If a triangle has an angle qθ with q ≥ 2, Mulan cuts it into angles θ and (q − 1)θ, reducing the multiple until a winning angle θ appears.The discarded triangle contains θ, while the remaining triangle retains a smaller positive multiple of θ.
  • Sufficiency: When no angle is a positive integer multiple of θ, Mulan’s special cut creates two triangles each containing such a multiple, allowing the game to enter the previous case.The resulting multiple is bounded by m − 1 when 180° = mθ, so the strategy terminates after finitely many moves.
  • Conclusion: Mulan can guarantee victory in finitely many steps if and only if θ divides 180°.This combines the impossibility result for non-divisors with the constructive strategy for divisors.
Loading 2609.11319v1…