Sage：带语义校正的形式化

# Sage:Formalization with Semantic Correction
Source: [https://arxiv.org/html/2609.35790](https://arxiv.org/html/2609.35790)
Farzad Jafarrahmani11footnotemark:1Abdelmouksit SagueniXiang ZhouWenping DengLiang ZhangHuawei Lagrange MathematicsComputing Research CenterAffiliation:Paris, France

###### Abstract

While neural theorem provers have achieved impressive milestones in formal mathematics, they largely operate on the assumption that faithful Lean 4 formal statements are already provided\. Translating informal natural language into a formal language is a critical data bottleneck plagued by an “illusion of rigor”: standard type\-checkers accept statements that compile but drop hypotheses, introduce vacuous truths, or subtly alter mathematical bounds\. To resolve this, we introduceSage\(Semantic Agent\-Guided Formalization Engine\), an agentic framework that replaces monolithic translation with a four\-stage decomposed generation pipeline coupled with a dual\-signal semantic correction loop\. By pairing Lean 4 compiler diagnostics with multi\-dimensional semantic feedback, our correction loop enforces mathematical fidelity alongside syntactic validity\. By explicitly accounting for the gap between open\-ended queries and declarative formal targets, our pipeline prevents models from achieving high formalization rates by guessing unverified answers \(exhibiting a70\.9%70\.9\\%answer leakage rate\)\. Consequently,Sagesuppresses leakage to2\.7%2\.7\\%while achieving73\.3%73\.3\\text\{\\,\}\\mathrm\{\\%\}pass@4 joint compilation and semantic fidelity on theOmni\-MATHwithout proofs \(compared to42\.0%42\.0\\%for a fine\-tunedGoedel\-Formalizer\-V2baseline\)\. Finally, onIMO\-Unformalized, a novel frontier of 175 unformalized International Mathematical Olympiad problems,Sagedemonstrates effective zero\-shot generalization with87\.4%87\.4\\text\{\\,\}\\mathrm\{\\%\}pass@4 verified fidelity compared to just19\.4%19\.4\\text\{\\,\}\\mathrm\{\\%\}for the baseline, winning over79%79\\text\{\\,\}\\mathrm\{\\%\}of blind pairwise evaluations\.

## 1Introduction

Informal statementSNLS\_\{\\mathrm\{NL\}\}*There are infinitely many prime numbers\.*Formal statementSFS\_\{\\mathrm\{F\}\}theorem infinitely\_many\_primes : ∀\\forallN,∃\\existsp≥\\geqN, Nat\.Prime p := by sorryTranslation

Figure 1:An example of autoformalization\. The system must faithfully encode the problem’s semantics into a Lean 4 theorem, explicitly omitting the proof \(sorry\) for downstream provers\.SNLS\_\{\\mathrm\{NL\}\}PNLP\_\{\\mathrm\{NL\}\}\(opt\.\)DistillerPreprocessorFormalizerFormatterSFS\_\{\\mathrm\{F\}\}\(a\)Decomposed generation stages\.SFS\_\{\\mathrm\{F\}\}SyntaxVerifierSemanticRaterRater’sCorrectionVerifierCompile∧\\wedgeRatings Ok?StatementCorrectorSF∗S\_\{F\}^\{\\ast\}NoYesNext round\(BudgetTT\)\(b\)Correction loop architecture\.
Figure 2:Overview ofSage, detailing the multi\-stage generation chain\([2\(a\)](https://arxiv.org/html/2609.35790#S1.F2.sf1)\)and syntax/semantic feedback loop\([2\(b\)](https://arxiv.org/html/2609.35790#S1.F2.sf2)\)\. Blue: Large Language Model agents; orange: verifiers\.Neural theorem provers and olympiad\-scale systems such as Goedel\-Prover\([Lin et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib28)\), DeepSeek\-Prover\([Ren et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib24)\)and AlphaProof\([Hubert et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib26)\)have pushed automated reasoning in Lean\([de Moura and Ullrich, 2021](https://arxiv.org/html/2609.35790#bib.bib6)\), yet their benchmarks largely assume the formal statementSFS\_\{\\mathrm\{F\}\}is already given and focus solely on finding a formal proof \(SF→PFS\_\{\\mathrm\{F\}\}\\to P\_\{\\mathrm\{F\}\}\)\. In practice, competition problems, textbooks, and user\-facing assistants arrive as informal natural languageSNLS\_\{\\mathrm\{NL\}\}; translatingSNL→SFS\_\{\\mathrm\{NL\}\}\\to S\_\{\\mathrm\{F\}\}\([Figure1](https://arxiv.org/html/2609.35790#S1.F1)\)111Throughout this paper, we use the terms*formalization*and*autoformalization*interchangeablywith*semantic fidelity*is the mandatory upstream step and a bottleneck for high\-quality formal training data\. A faithfulSFS\_\{\\mathrm\{F\}\}is the contract under which every downstream prover, benchmark, and library entry must operate—yet the field lacks a shared account of what that contract*contains*beyond “it type\-checks\.” Crucially, compile success is not semantic fidelity: Lean 4 accepts statements that compile but fundamentally*misstate*the problem\. For example, if a model drops a crucial minimality condition, the resulting bare existential type\-checks perfectly withsorry\. Compilers cannot detect semantic mismatches, leaving standard compile\-only repair loops blind to dropped hypotheses, introduced tautologies \(True\), and vacuous placeholders\.

##### Our approach\.

To address this, we introduceSage\(Semantic Agent\-Guided Formalization Engine\), an agentic framework shifting autoformalization from monolithic generation to iterative semantic correction\.Sagedecomposes formalization into four inspectable stages \(distillation, preprocessing, formalization, formatting\) and refines candidates via a dual\-signal correction loop combining compiler diagnostics with multi\-dimensional semantic feedback\. To support distinct downstream applications,Sageprovides two configurations:Answer\-Aware\(leveraging informal proofs to curate resolved, prover\-ready targets\) andAnswer\-Agnostic\(translating problem text alone without proof oracles or solutions\)\. Our contributions are as follows:

1. 1\.Theoretical Foundations:We formalize the distinction between Assertion\- and Question\-type mathematics, exposing the*Discovery Trap*and type\-theoretic vulnerabilities that arise when translating open queries without proof oracles\.
2. 2\.Decomposed Generation Pipeline:We introduce a modular four\-stage formalization protocol that decouples goal extraction, typing, and syntax generation, isolating structural constraints and eliminating unmonitored answer guessing\.
3. 3\.Multi\-Dimensional Semantic Feedback:We define an actionable rubric tracking critical axes of translation divergence—including dropped hypotheses, altered bounds, and vacuous placeholders—operationalized into a test\-time semantic evaluator\.
4. 4\.Dual\-Signal Correction Loop:Our iterative repair loop pairs Lean 4 compiler diagnostics with semantic feedback, correcting subtle mathematical flaws that type\-checkers overlook\.

Empirically,Sageoutperforms zero\-shot generation, syntax\-only repair loops, and fine\-tuned baselines\. OnOmni\-MATHwithout proofs,Sagesuppresses unmonitored answer leakage from70\.9%70\.9\\text\{\\,\}\\mathrm\{\\%\}to2\.7%2\.7\\text\{\\,\}\\mathrm\{\\%\}, while nearly doubling the fine\-tunedGoedel\-Formalizer\-V2baseline in verified formalization \(73\.3%73\.3\\text\{\\,\}\\mathrm\{\\%\}vs\.42\.0%42\.0\\text\{\\,\}\\mathrm\{\\%\}pass@4;50\.3%50\.3\\text\{\\,\}\\mathrm\{\\%\}vs\.26\.7%26\.7\\text\{\\,\}\\mathrm\{\\%\}pass@1\)\. On the unformalized IMO frontier \(IMO\-Unformalized\),Sageachieves87\.4%87\.4\\text\{\\,\}\\mathrm\{\\%\}pass@4 verified fidelity \(vs\.19\.4%19\.4\\text\{\\,\}\\mathrm\{\\%\}for the baseline\), winning over79%79\\text\{\\,\}\\mathrm\{\\%\}of blind pairwise head\-to\-head comparisons\.

[Section2](https://arxiv.org/html/2609.35790#S2)situates our work in autoformalization and self\-refinement;[Section3](https://arxiv.org/html/2609.35790#S3)formalizes the theoretical limits of translation;[Sections4](https://arxiv.org/html/2609.35790#S4)and[5](https://arxiv.org/html/2609.35790#S5)describe the approach and evaluation design;[Section6](https://arxiv.org/html/2609.35790#S6)reports results; and[Sections7](https://arxiv.org/html/2609.35790#S7)and[8](https://arxiv.org/html/2609.35790#S8)discuss limitations and conclude\.

## 2Related Work

Neural Theorem Proving and the Statement BottleneckWhile progress in automated theorem proving has yielded olympiad\-scale systems\([Hubert et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib26);[Lin et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib28);[Ren et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib24)\)and advanced search/RL tactic methods\([Yang et al\., 2023](https://arxiv.org/html/2609.35790#bib.bib29);[Lample et al\., 2022](https://arxiv.org/html/2609.35790#bib.bib13);[Zhou et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib23);[Chen et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib27)\), most systems assume a pre\-given formal statementSFS\_\{\\mathrm\{F\}\}\(SF→PFS\_\{\\mathrm\{F\}\}\\to P\_\{\\mathrm\{F\}\}\)\. Relying on human translation \(SNL→SFS\_\{\\mathrm\{NL\}\}\\to S\_\{\\mathrm\{F\}\}\)\([Zheng et al\., 2022](https://arxiv.org/html/2609.35790#bib.bib14);[Liu et al\., 2023](https://arxiv.org/html/2609.35790#bib.bib15)\)is fragile: statement errors propagate silently to downstream provers\([Ammanamanchi et al\., 2026](https://arxiv.org/html/2609.35790#bib.bib9)\), requiring retroactive benchmark corrections\([Ospanov et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib8);[Poiroux et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib7)\)\. We directly target this upstream translation bottleneck\.

Autoformalization: From Natural Language to Formal StatementsAlthough autoformalization predates Large Language Models\([Wang et al\., 2018](https://arxiv.org/html/2609.35790#bib.bib10)\), recent LLM\-driven advances\([Wu et al\., 2022](https://arxiv.org/html/2609.35790#bib.bib4)\)leverage formal benchmarks\([Azerbayev et al\., 2024a](https://arxiv.org/html/2609.35790#bib.bib31);[Ying et al\., 2024](https://arxiv.org/html/2609.35790#bib.bib32);[Gao et al\., 2024](https://arxiv.org/html/2609.35790#bib.bib33)\), retrieval agents\([Wang et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib25)\), and specialized foundation models\([Azerbayev et al\., 2024b](https://arxiv.org/html/2609.35790#bib.bib11);[Wang et al\., 2024a](https://arxiv.org/html/2609.35790#bib.bib12)\)\. However, monolithic single\-prompt translations frequently drop hypotheses, conflate premises, or misinterpret domain bounds\. To evaluate semantic faithfulness, FormalAlign\([Lu et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib2)\)aligns representation spaces while[Liu et al\. \(2025\)](https://arxiv.org/html/2609.35790#bib.bib3)introduce BEq for formal\-grounded equivalence\.

Multi\-Agent Decomposition and Iterative RefinementModular generation and multi\-agent coordination enhance complex reasoning\([Ridnik et al\., 2024](https://arxiv.org/html/2609.35790#bib.bib16);[Lightman et al\., 2024](https://arxiv.org/html/2609.35790#bib.bib17);[Wang et al\., 2024b](https://arxiv.org/html/2609.35790#bib.bib18);[Hong et al\., 2024](https://arxiv.org/html/2609.35790#bib.bib19);[Wu et al\., 2024](https://arxiv.org/html/2609.35790#bib.bib20)\), while iterative refinement frameworks\([Madaan et al\., 2023](https://arxiv.org/html/2609.35790#bib.bib30);[Shinn et al\., 2023](https://arxiv.org/html/2609.35790#bib.bib21);[Gou et al\., 2024](https://arxiv.org/html/2609.35790#bib.bib22)\)leverage tool feedback\. Yet standard code loops fail in formal math: targeting compilation alone causes models to strip constraints to appease type\-checkers, destroying semantic fidelity\. ReForm\([Chen et al\., 2026](https://arxiv.org/html/2609.35790#bib.bib1)\)addresses this via reflective semantic consistency checks\. We combine structured decomposition with iterative, semantics\-aware refinement to correct statements at the component level\.

## 3Formalizing Mathematics: Beyond Naive Translation

Autoformalization is a constrained translation task: mapping informal mathematical language \(English\) into a formal language such as dependent type theory in Lean 4\. A successful formalization must satisfy the following desiderata:

1. 1\.Syntactic validity:the statement must be well\-typed in the target system and respect the*single\-sorry contract*:SFS\_\{\\mathrm\{F\}\}must contain strictly one terminating placeholder \(:= by sorry\) closing the main theorem proof\.
2. 2\.Semantic fidelity:the statement must preserve the mathematical meaning of the source\.
3. 3\.Texture:the formalization should respect the pragmatic structure of the source—whether the informal text asserts a declarative claim to be verified, or poses an open\-ended question asking for a value, witness, or polarity\.

We call the second dimension*semantic match*\. In[Section4\.3](https://arxiv.org/html/2609.35790#S4.SS3),Sage\-SMserves as an in\-loop fidelity metric to gate our correction loop, and we adopt the existingGoedel\-SMprotocol as a post\-hoc judge\.

##### Assertion\-Type and Question\-Type Statements: The Discovery vs\. Verification Gap

A useful distinction for autoformalization is between*Assertion\-type*and*Question\-type*statements\. AnAssertion\-type statementalready presents a complete mathematical claim to be verified \(e\.g\., “Show that…” or “Prove that…”\)\. By contrast, aQuestion\-type statementasks for an unknown object, value, witness, or characterization \(e\.g\., “Find…”, “Determine…”\)\.

This exposes the*Discovery vs\. Verification Gap*: natural language math poses open\-ended*discovery*problems, whereas theorem provers like Lean 4 require strict*verification*\. Formalizing open queries intotheoremstatements forces pre\-guessing answers, rendering the simultaneous satisfaction of all three translation dimensions often impossible\. Consequently, for question\-type statements, preserving original*texture*and ensuring*semantic fidelity*work at cross\-purposes, exposing how verification systems fundamentally struggle with mathematical discovery\.

##### The Feasibility Trilemma

To bridge this gap and convert open questions into declarative targets, we identify three distinct formalization strategies, each presenting a different trade\-off between semantic match and downstream prover usability\. Canonical encodings for an abstract query are contrasted in[Table1](https://arxiv.org/html/2609.35790#S3.T1):

1. 1\.Explicit Answer Injection:Incorporates the resolved answer directly into the statement, rewriting the open question as a concrete assertion\. - •Pros:Produces clean, fully specified declarative theorems ready for downstream tactic provers\. - •Cons:Requires an oracle or proof context to resolve the value prior to formalization, completely breaking the open\-ended texture of the original query\.
2. 2\.Placeholder Definitions:Introduces a typed, unresolved constant via a placeholder stub, asserting the desired properties about that constant in the theorem\. - •Pros:Formalizable without prior knowledge of the answer while preserving original texture\. - •Cons:Forces proving agents to modify the source code \(instantiating the placeholder\), violating the read\-only contract of automated theorem proving\.
3. 3\.Existential Encoding:Reformulates the query as an existential proposition over the constraints, delegating constructive witness search to the downstream prover\. - •Pros:Faithfully captures open\-ended natural language intent without an answer oracle\. - •Cons:Highly fragile when applied to polar queries and susceptible to computational bypass in characterization queries \(the*Triviality Trap*; see[SectionA\.3](https://arxiv.org/html/2609.35790#A1.SS3)\)\.

We unify this fundamental trade\-off: an answer\-agnostic autoformalizer cannot map an open interrogative query into a single declarative proposition without assuming an oracle, breaking prover usability, or introducing logical vulnerabilities\.

Table 1:The Formalization Feasibility Trilemma across Question Types\.StrategyLean 4 Formalization Example\(SNLS\_\{\\mathrm\{NL\}\}: Find an objectxxof typeα\\alphathat satisfies the propertyPP\)SyntacticValidity?SemanticFidelity?PreservesTexture?RequiresOracle?Explicit Answertheorem target : P c := by sorryYesYesNoYesPlaceholderdef x :α\\alpha:= sorrytheorem target : P x := by sorryBreaksRead\-OnlyYesYesNoExistentialtheorem target :∃\\existsx :α\\alpha, P x := by sorryYesVulnerableYesNo

Crucially, reducing open interrogative queries to standardPropexistentials allows automated provers to bypass constructive search via syntactic shortcuts, such as the*Polarity Cheat*and the*Triviality Trap*\. To prevent this, we propose*Type\-Theoretic Locks*to structurally enforce witness synthesis\. WithinSage, our Formalizer and in\-loop Rater actively apply lock\-aware rules to steer candidate statements away from trivialized encodings: where feasible, the pipeline attempts to harden statements into locked formulations, otherwise defaulting to a standard existential\. We detail the underlying mechanics, criteria, and reference Lean 4 lock implementations in[AppendixA](https://arxiv.org/html/2609.35790#A1)\.

Rather than treating this trilemma as an insurmountable barrier,Sagedeliberately navigates it by supporting two distinct operating configurations\. In theAnswer\-Agnostic \(Fidelity\-Oriented\)regime, we adopt*Existential Encodings*to strictly preserve query texture and prevent answer leakage\. Conversely, in theAnswer\-Aware \(Prover\-Oriented\)regime, we utilize*Explicit Answer Injection*guided by an informal proof, providing automated tactic engines with the fully resolved, concrete goals they require\.

## 4TheSageFramework: Composition & Semantic Correction

To translate natural language statements into Lean 4 while avoiding the logical omissions and silent failures typical of single\-pass generation, we present theSageframework\. It decomposes the translation and verification task into three sequential phases inspired by classical compiler design:Draft\(Compositional Generation\),Verify\(Multi\-Dimensional Statement Verification\), andRefine\(Semantic Correction Loop\)\.

### 4\.1Compositional Generation \(The Draft Phase\)

Given an informal statementSNLS\_\{\\mathrm\{NL\}\}and an optional informal proofPNLP\_\{\\mathrm\{NL\}\}, generation maps\(SNL,PNL​?\)→SF\(S\_\{\\mathrm\{NL\}\},P\_\{\\mathrm\{NL\}\}?\)\\to S\_\{\\mathrm\{F\}\}through four specialized, role\-isolated agents \([Figure2\(a\)](https://arxiv.org/html/2609.35790#S1.F2.sf1)\):

1. 1\.Distiller:EvaluatesSNLS\_\{\\mathrm\{NL\}\}and informal proofPNLP\_\{\\mathrm\{NL\}\}\(when available\)\. In the answer\-aware regime, it classifies the problem type \(Assertion\- vs\. Question\-type\) and extracts the target witness or characterization from the proof as an Inferred Goal; in the answer\-agnostic regime, it reformulates open interrogative queries into explicit declarative targets without an answer oracle\.
2. 2\.Preprocessor:StandardizesSNLS\_\{\\mathrm\{NL\}\}via information provided by the distiller into a pseudocode representation, isolating supporting mathematical definitions, localized hypotheses \(h1,…,hnh\_\{1\},\\dots,h\_\{n\}\), and the target conclusion \(GG\)\.
3. 3\.Formalizer:Translates the preprocessed pseudocode into idiomatic Lean 4 declarations and theorem signatures, leveraging standardizedMathlibabstractions\([The mathlib Community, 2020](https://arxiv.org/html/2609.35790#bib.bib5)\)while avoiding trivialization stubs\.
4. 4\.Formatter:Performs syntactic sanitization and assembly, organizing imports, namespaces, andnoncomputablesections to ensure the draft is a standalone, compilable Lean 4 file without altering its mathematical semantics\.

We provide the details of each agent in[SectionB\.1](https://arxiv.org/html/2609.35790#A2.SS1)as well as a step\-by\-step walkthrough across both regimes onOmni\-MATH\#043 in[SectionB\.5](https://arxiv.org/html/2609.35790#A2.SS5)\([Figure4](https://arxiv.org/html/2609.35790#A2.F4)\)\.

##### Syntax Verification and the Single\-Sorry Invariant

An external Lean 4 verifier evaluates each candidate statementSFS\_\{\\mathrm\{F\}\}, passingCompileif syntactically valid and well\-typed\. Targeting statement formalization rather than proof search, theorem bodies are deferred using Lean’ssorryplaceholder\. When compilation fails, structured error diagnostics \(line, column, messages\) are intercepted and routed directly to the correction loop \([Section4\.3](https://arxiv.org/html/2609.35790#S4.SS3)\)\.

Beyond type\-checking, a*prover\-ready*formalization should obey the*single\-sorry contract*:SFS\_\{\\mathrm\{F\}\}contains exactly one terminating placeholder \(:= by sorry\) on the main theorem\. Additional placeholders \(sorry,admit,axiom\)—such as in stubbed definitions or auxiliary lemmas—leave the target underspecified for a read\-only downstream prover \(we audit this failure in[SectionC\.4](https://arxiv.org/html/2609.35790#A3.SS4)\)\.

### 4\.2Multi\-Dimensional Alignment Criteria

Compilation guarantees type validity, but cannot verify faithfulness to the informal source: a draft may drop critical hypotheses or trivialise the claim while type\-checking perfectly undersorry\. To detect these silent translational failures,Sageintroduces a semanticRaterthat auditsSFS\_\{\\mathrm\{F\}\}againstSNLS\_\{\\mathrm\{NL\}\}across three complementary axes:

##### Modular Component Matching\.

Suppose informal statementSNLS\_\{\\mathrm\{NL\}\}decomposes into componentsCNL=\{c1,c2,c3\}C\_\{\\mathrm\{NL\}\}=\\\{c\_\{1\},c\_\{2\},c\_\{3\}\\\}\. The formalized componentsCFC\_\{\\mathrm\{F\}\}inSFS\_\{\\mathrm\{F\}\}are audited against three failure modes:

- •Missing \(CF=\{c1,c2\}C\_\{\\mathrm\{F\}\}=\\\{c\_\{1\},c\_\{2\}\\\}\):A necessary component \(c3c\_\{3\}\) is omitted\. The rater separates explicit omissions from acceptable implicit captures \(e\.g\., bounds handled natively by Lean’s type system\)\.
- •Wrong \(CF=\{c1,c2′,c3\}C\_\{\\mathrm\{F\}\}=\\\{c\_\{1\},c\_\{2\}^\{\\prime\},c\_\{3\}\\\}\):A component is mapped to an incorrect, inverted, or flawed representation \(c2′c\_\{2\}^\{\\prime\}instead ofc2c\_\{2\}\), measuring translational misalignment rather than mere omission\.
- •Extra \(CF=\{c1,c2,c3,c4\}C\_\{\\mathrm\{F\}\}=\\\{c\_\{1\},c\_\{2\},c\_\{3\},c\_\{4\}\\\}\):A spurious component \(c4c\_\{4\}\) is introduced\. The rater flags additions restricting theorem scope, altering truth value, or causing vacuous provability\.

Intended Premises \(CNLC\_\{\\mathrm\{NL\}\}\)
c0:f:\[0,1\]→ℝc\_\{0\}\\colon f\\colon\[0,1\]\\to\\mathbb\{R\}c1:f⁡\(0\)=0c\_\{1\}\\colon f\(0\)=0c2:f​is increasingc\_\{2\}\\colon f\\text\{ is increasing\}Goal:f⁡\(x\)≥0f\(x\)\\geq 0Formalized Premises \(CFC\_\{\\mathrm\{F\}\}\)
c0:f:\[0,2\]→ℝc\_\{0\}\\colon f\\colon\[0,\{\\color\[rgb\]\{1,0,0\}2\}\]\\to\\mathbb\{R\}\[Wrong\]
c1:f⁡\(0\)=0c\_\{1\}\\colon f\(0\)=0
c2:f​is increasingc\_\{2\}\\colon f\\text\{ is increasing\}\[Missing\]
c3:f′​\(0\)=0c\_\{3\}\\colon f^\{\\prime\}\(0\)=0\[Extra\]
Goal:f⁡\(x\)≥0f\(x\)\\geq 0TranslationFigure 3:Contextual Integrity Failure Modes\.
##### Holistic Mathematical Equivalence\.

Audits the statement as an integrated whole rather than isolated components, ensuringSFS\_\{\\mathrm\{F\}\}preserves the intended assertions and logical structure ofSNLS\_\{\\mathrm\{NL\}\}\.

- •Semantic Match:Evaluates translational equivalence betweenSFS\_\{\\mathrm\{F\}\}andSNLS\_\{\\mathrm\{NL\}\}, verifying that all concepts, relations, and objectives are faithfully captured while penalizing discrepancies or artificial trivializations regardless of underlying truth value\.
- •Exactness:Measures structural and stylistic alignment withSNLS\_\{\\mathrm\{NL\}\}, distinguishing direct, literal translation from logically equivalent restatements or Mathlib\-idiomatic forms\.

##### Code Implementation Quality\.

Beyond semantic equivalence, this dimension evaluates whether formal code adheres to idiomatic library conventions and robust abstraction design:

- •Naturality:Evaluates Lean 4 style, mathematical generality, andMathlibreuse, penalizing ad\-hoc reinventions of library structures\. For instance, expandingMonotone finto raw inequalities \(∀x≤y,f⁡\(x\)≤f⁡\(y\)\\forall x\\leq y,f\(x\)\\leq f\(y\)\) prevents tactics likesimpandgcongrfrom recognizing properties, blocking provers from leveraging existingMathliblemmas\.
- •Descriptive Precision:Audits how deeply informal prose \(e\.g\., algorithms, geometric shapes or constructions\) is formalized, ensuring concepts are modeled fundamentally rather than bypassed via trivial definitions orsorrystubs\.

While the Lean 4 compiler handles basic compilation, our criteria ensure full semantic fidelity\.[Section4\.3](https://arxiv.org/html/2609.35790#S4.SS3)details the correction loop that repairs syntax errors and semantic flaws together\.

### 4\.3Semantic Correction Loop

To close the gap between type\-checking and mathematical meaning,Sagerefines each draft for up toTTrounds under a joint gate \([Figure2\(b\)](https://arxiv.org/html/2609.35790#S1.F2.sf2)\)\. A candidate exits successfully only when it satisfiesCompile∧\\wedgeSage\-SM, i\.e\., it type\-checks and passes the in\-loop semantic checkSage\-SMderived from the dimensions in[Section4\.2](https://arxiv.org/html/2609.35790#S4.SS2)\.

Compile\-only repair often restores well\-typedness by deleting or trivializing hypotheses, destroying the intended meaning\. OurCorrectortherefore receives a*dual signal*at each round—Lean diagnostics together with the Rater’s failing dimensions, scores, and rationales—and is steered toward a semantic baseline: the Rater proposes a repair draft for the Corrector to refine, reconciling type errors without solving the underlying math or injecting concrete answers\. Engineering stabilizations of this loop \(cascading\-error triage; pre\-compilation of Rater\-proposed drafts; Corrector contracts\) are detailed in[SectionB\.2](https://arxiv.org/html/2609.35790#A2.SS2)\.

## 5Experimental Setup

##### Datasets

We evaluate across three complementary benchmarks spanning distinct problem textures and formalization frontiers\. First,Omni\-MATH\(N=300N=300\)\([Gao et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib35)\)evaluates the standardized 300\-problem competition subset from[Lin et al\. \(2025\)](https://arxiv.org/html/2609.35790#bib.bib28), dominated by open\-ended*question\-type*queries \(98\.7%98\.7\\text\{\\,\}\\mathrm\{\\%\}\)\. Second, we curate two complementary IMO suites from a July 2026 snapshot of the community[compfiles](https://github.com/dwrensha/compfiles)repository\([Renshaw, 2024](https://arxiv.org/html/2609.35790#bib.bib34)\)\(398398historical problems from 1959 to 2024\):IMO\-Formalized\(N=223N=223;48\.4%48\.4\\text\{\\,\}\\mathrm\{\\%\}assertion\-type\) comprises all problems with official human\-verified Lean 4 formalizations; andIMO\-Unformalized\(N=175N=175;64\.0%64\.0\\text\{\\,\}\\mathrm\{\\%\}assertion\-type\) comprises the remaining unformalized frontier\. Full curation protocols, domain breakdowns, and texture statistics are detailed in[SectionC\.1](https://arxiv.org/html/2609.35790#A3.SS1)\.

##### Method Variants

We evaluate our framework across both monolithic and decomposed architectures under matched iteration budgets \(T∈\[5,10\]T\\in\[5,10\]\):

- •Monolithic:Operates zero\-shot in a single generation pass without pipeline decomposition\.
- •Decomposed:Follows our modular four\-stage generation pipeline introduced in[Section4\.1](https://arxiv.org/html/2609.35790#S4.SS1)\.
- •Feedback Loops:For both architectures, we evaluate single\-pass generation \(no feedback\), a syntax\-only repair loop \(compiler diagnostics\), and our full dual\-signal semantic correction loop \(compiler errors plusSage\-SMratings\)\.

Sagedenotes the completeDecomposed\+Semanticconfiguration, evaluated againstGoedel\([Lin et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib28)\)as an external domain\-specialized monolithic baseline\.[Table10](https://arxiv.org/html/2609.35790#A3.T10)details all evaluated configurations and hyperparameters\.

### 5\.1Evaluation Metrics

Evaluating autoformalization requires moving beyond compilation to catch semantic drift, vacuous proofs from placeholder misuse, and unmonitored answer guessing\. Assessing true translation fidelity demands tracking syntactic validity, structural integrity, and mathematical alignment in tandem \([SectionC\.4](https://arxiv.org/html/2609.35790#A3.SS4)details audit protocols, rubrics, and consensus rules\):

- •Compilation \(Compile\):Fraction of generated formalizations type\-checking in Lean 4 with Mathlib, deferring proof bodies via thesorryplaceholder\.
- •Multiple Sorries Rate:Uses syntactic pattern matching to measure the fraction of candidates containing\>1\>1sorryplaceholder, identifying outputs that evade difficulty by stubbing unresolved definitions or unproven helper lemmas\.
- •Answer Leakage Audit:For proofless open\-ended questions, an independent LLM auditor inspects whether models cheated by prematurely injecting the target mathematical witness or numerical answer into the theorem signature\.
- •Post\-Hoc Semantic Match \(Goedel\-SM\):Evaluates external semantic fidelity via unanimous4/44/4consensus from an independent Gemma4\-31B judge following[Lin et al\. \(2025\)](https://arxiv.org/html/2609.35790#bib.bib28)\.
- •In\-Loop Semantic Gate \(Sage\-SM\):Assesses candidate formalizations across our rubrics \([Section4\.2](https://arxiv.org/html/2609.35790#S4.SS2)\) to direct the correction loop and filter high\-trust formal targets\.
- •Pairwise Win Rate \(PWR\):Measures relative semantic superiority by aggregating blind, order\-swapped head\-to\-head comparisons scored on a 5\-point preference scale by an independent judge\.
- •Joint Success \(Compile∧\\wedgeGoedel\-SM\):Primary benchmark metric, requiring candidate formalizations to simultaneously compile and attain unanimous post\-hoc semantic consensus\.

Unless otherwise stated, all metrics are percentages where higher is better \(↑\\uparrow\);bolddenotes the best\-performing result in each column\.

## 6Results and Analysis

We evaluateSageand baseline variants acrossOmni\-MATH,IMO\-Formalized, andIMO\-Unformalizedto answer three core questions:

1. 1\.Syntax vs\. Semantics:How effectively does semantic feedback close the gap between code compilation and mathematical correctness?
2. 2\.Autonomous Zero\-Shot Formalization:Without access to proofs or solutions, how reliably can models translate genuine competition theorems into verified Lean 4 code?
3. 3\.Translating vs\. Guessing:Do baseline models genuinely translate open competition problems, or are they secretly guessing answers \(and creating false mathematical claims\)?

Human Validation of the Semantic EvaluatorWe validate the automated semantic gate via a stratified adversarial audit \(N=45N=45zero\-shotOmni\-MATHdrafts, deliberately oversampling silent semantic failures;[AppendixE](https://arxiv.org/html/2609.35790#A5)\)\. Three Lean\-proficient annotators independently scored each candidate draft\. Prioritizing mathematical correctness over Lean implementation aesthetics, annotators evaluated drafts strictly against the five core semantic criteria \(Missing, Wrong, Extra, Semantic Match, Exactness\) and their joint binary gate, omitting code\-quality dimensions \(Naturality and Descriptive Precision\)\. Taking the human majority binary decision as the reference, the automated gate achieves71\.1%71\.1\\text\{\\,\}\\mathrm\{\\%\}agreement, with mean human Semantic Match correlating with the automated rater at Spearmanρ=0\.63\\rho=0\.63\(Pearsonr=0\.64r=0\.64\)\.

### 6\.1Prover\-Ready Formalization: Answer\-Aware Translation

We first evaluate the*answer\-aware*setting, where informal statementSNLS\_\{\\mathrm\{NL\}\}includes proof/solutionPNLP\_\{\\mathrm\{NL\}\}\([Table3](https://arxiv.org/html/2609.35790#S6.T3)\)\. Targeting verified training corpus curation for downstream provers\([Hubert et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib26);[Lin et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib28)\),PNLP\_\{\\mathrm\{NL\}\}supplies necessary witnesses and constants for high\-fidelity translation into compiling, declarative Lean 4 code\.

Table 2:Formalization quality onOmni\-MATH\(Answer\-Aware, pass@1\)\.∗In\-loop optimization target\.MethodCompileCompile∧\\wedgeGoedel\-SMCompile∧\\wedgeSage\-SM∗Monolithic PipelineBase Generation73\.054\.357\.7\+ Syntax Loop96\.074\.373\.3\+ Semantic Loop97\.376\.396\.3∗Decomposed PipelineBase Generation68\.052\.754\.7\+ Syntax Loop95\.075\.074\.7\+ Semantic Loop96\.077\.393\.7∗
Table 3:Base model scaling underSageonOmni\-MATH\(Answer\-Aware, pass@1\)\.Repair budgetT=5T=5\. Default backbone is Qwen3\.6\-27B\.UnderlyingModelCompileCompile∧\\wedgeGoedel\-SMCompile∧\\wedgeSage\-SM∗AverageRepairs \(↓\\downarrow\)Qwen3\-32B57\.330\.352\.33\.2Qwen3\.6\-27B96\.077\.393\.71\.1Qwen3\.8\-27B98\.085\.795\.71\.1

Syntax vs\. Semantic AttributionAs shown in[Table3](https://arxiv.org/html/2609.35790#S6.T3), unguided base drafts leave a substantial compilation deficit \(73\.0%73\.0\\text\{\\,\}\\mathrm\{\\%\}for monolithic,68\.0%68\.0\\text\{\\,\}\\mathrm\{\\%\}for decomposed\), limiting joint success \(Compile∧\\wedgeGoedel\-SM\) to54\.3%54\.3\\text\{\\,\}\\mathrm\{\\%\}and52\.7%52\.7\\text\{\\,\}\\mathrm\{\\%\}\. Adding compiler feedback alone \(Monolithic\+SyntaxandDecomposed\+Syntax\) resolves the vast majority of mechanical typing and environment errors, lifting compilation above95%95\\text\{\\,\}\\mathrm\{\\%\}and joint fidelity to74\.3%74\.3\\text\{\\,\}\\mathrm\{\\%\}–75\.0%75\.0\\text\{\\,\}\\mathrm\{\\%\}\. These syntax\-only variants iteratively repair drafts using Lean diagnostics alone—with the same cascading\-error triage as the full loop, but no semantic rater—and terminate onCompile\(details in[SectionB\.3](https://arxiv.org/html/2609.35790#A2.SS3)\)\. Integrating multi\-dimensional semantic feedback \(Sage\) provides the final precision filter, catching remaining hypothesis omissions and reaching77\.3%77\.3\\text\{\\,\}\\mathrm\{\\%\}joint fidelity on the externalGoedel\-SMjudge and93\.7%93\.7\\text\{\\,\}\\mathrm\{\\%\}under the multi\-dimensionalSage\-SMgate\.

Monolithic vs\. Decomposed Trade\-offsWhen informal proofs are available, monolithic and decomposed semantic loops achieve comparable top\-line accuracy \(76\.3%76\.3\\text\{\\,\}\\mathrm\{\\%\}vs\.77\.3%77\.3\\text\{\\,\}\\mathrm\{\\%\}\), as the provided proof eliminates ambiguity around target constants\. In this proof\-guided regime, the primary advantage of decomposition is structural auditability through inspectable intermediate representations\. Crucially, as we show in[Section6\.3](https://arxiv.org/html/2609.35790#S6.SS3), the decisive mathematical necessity of decomposition emerges when proofs are absent: without an answer oracle, monolithic generation collapses into unmonitored answer guessing, whereas decomposition enforces genuine translation\.

Base Model Scaling DynamicsBase model ablation \([Table3](https://arxiv.org/html/2609.35790#S6.T3)\) reveals monotonic scaling: joint verified fidelity rises from30\.3%30\.3\\text\{\\,\}\\mathrm\{\\%\}on the weakest model \(Qwen3\-32B\) to85\.7%85\.7\\text\{\\,\}\\mathrm\{\\%\}on the strongest \(Qwen3\.8\-27B\)\. Simultaneously, average repair rounds drop from 3\.2 to∼\\sim1\.1 on modern backbones, showing that the framework scales directly with base model capability\.

### 6\.2Autonomous Zero\-Shot Formalization across the IMO Landscape

We next evaluate autonomous formalization without proof oracles \(SNLS\_\{\\mathrm\{NL\}\}only\) on International Mathematical Olympiad problems \([Table4](https://arxiv.org/html/2609.35790#S6.T4)\), testing whether systems can faithfully translate competition\-grade mathematics zero\-shot\.

Table 4:Formalization quality across the IMO landscape \(Answer\-Agnostic\)\.pass@1pass@4MethodCompileGoedel\-SMCompile∧\\wedgeGoedel\-SMCompileCompile∧\\wedgeGoedel\-SMIMO\-Formalized\(N=223N=223, Established Benchmark\)Monolithic\(Zero\-Shot\)72\.657\.443\.083\.962\.3Goedel\-Formalizer\-V2\(Baseline\)76\.744\.437\.290\.650\.7Sage\(Semantic Loop\)94\.265\.061\.499\.683\.9IMO\-Unformalized\(N=175N=175, Unformalized Frontier\)Monolithic\(Zero\-Shot\)58\.331\.420\.089\.733\.1Goedel\-Formalizer\-V2\(Baseline\)48\.015\.410\.386\.919\.4Sage\(Semantic Loop\)83\.472\.660\.096\.687\.4

Robust Generalization to Unformalized MathematicsMoving fromOmni\-MATHtoIMO\-Unformalized, the fine\-tunedGoedelbaseline collapses to10\.3%10\.3\\text\{\\,\}\\mathrm\{\\%\}joint fidelity \(Compile∧\\wedgeGoedel\-SM;[Table4](https://arxiv.org/html/2609.35790#S6.T4)\)\. Conversely,Sagegeneralizes robustly across the IMO landscape, achieving61\.4%61\.4\\text\{\\,\}\\mathrm\{\\%\}joint fidelity on establishedcompfilesbenchmarks \(IMO\-Formalized\) and60\.0%60\.0\\text\{\\,\}\\mathrm\{\\%\}on the unformalized frontier \(IMO\-Unformalized\)—a5\.8×5\.8\\timesgain over the baseline\. This parity confirms semantic correction does not rely on memorizing human formalizations or benchmark artifacts, transferring robustly to unformalized mathematics\.

Table 5:Blind pairwise preferences onIMO\-Unformalized\(Answer\-Agnostic, pass@1\)\.Preference forSageoverGoedel\(%\)Evaluation TypeMuch BetterBetterTieWorseMuch WorseSemantic \(PWR\)78\.31\.117\.71\.11\.7Blind Pairwise PreferenceOrder\-swapped pairwise evaluations by an independent judge corroborate these results beyond discrete metric thresholds \([Table5](https://arxiv.org/html/2609.35790#S6.T5)\):Sageis strictly preferred overGoedelin79\.4%79\.4\\text\{\\,\}\\mathrm\{\\%\}of matchups, with ties in17\.7%17\.7\\text\{\\,\}\\mathrm\{\\%\}and the baseline preferred in only2\.8%2\.8\\text\{\\,\}\\mathrm\{\\%\}\.

Takeaway\.On the unformalized IMO frontier,Sageachieves60\.0%60\.0\\text\{\\,\}\\mathrm\{\\%\}zero\-shot joint fidelity at pass@1 \(scaling to87\.4%87\.4\\text\{\\,\}\\mathrm\{\\%\}at pass@4\), outperforming the specialized baseline by nearly6×6\\times\.

### 6\.3The Discovery Trap: Unmasking Answer\-Agnostic Question Benchmarks

Because98\.7%98\.7\\text\{\\,\}\\mathrm\{\\%\}of the problems inOmni\-MATHare question\-type, the answer\-agnostic setting forces every method to confront the Feasibility Trilemma \([Section3](https://arxiv.org/html/2609.35790#S3)\): answer injection, placeholder definitions, or existential encoding\.[Table6](https://arxiv.org/html/2609.35790#S6.T6)reports the resulting quality scores\.

To ensure a strict, unbiased evaluation, we test against the established community metric \(Goedel\-SM\) rather than our internal gate, even though our reject audit \([Table11](https://arxiv.org/html/2609.35790#A3.T11)\) demonstrates thatGoedel\-SMsystematically penalizes legitimate existential translations\.

Table 6:Formalization quality onOmni\-MATH\(Answer\-Agnostic\)\.†Monolithic variants suffer from severe answer leakage \(\>70%\>70\\%, guessing unverified answers; see[Table7](https://arxiv.org/html/2609.35790#S6.T7)\)\.Sageis the top\-performing valid, leak\-free method\. Bold indicates best leak\-free performance\.pass@1pass@4MethodCompileCompile∧\\wedgeGoedel\-SMCompileCompile∧\\wedgeGoedel\-SMMonolithic†73\.040\.087\.359\.0Monolithic\+Semantic†95\.755\.399\.075\.0Decomposed62\.029\.785\.050\.7Decomposed\+Syntax95\.742\.799\.061\.7Decomposed\+Semantic\(Sage\)94\.750\.398\.773\.3Goedel\(Finetuned Baseline\)74\.026\.788\.342\.0WhileMonolithic\+Semanticseemingly outperformsSage\(55\.3%55\.3\\text\{\\,\}\\mathrm\{\\%\}vs\.50\.3%50\.3\\text\{\\,\}\\mathrm\{\\%\}joint pass@1\),[Table7](https://arxiv.org/html/2609.35790#S6.T7)reveals why:Monolithic\+Semanticinjects guessed numerals in70\.9%70\.9\\text\{\\,\}\\mathrm\{\\%\}of outputs versus2\.7%2\.7\\text\{\\,\}\\mathrm\{\\%\}forSage\. Low injection alone is incomplete, as models could suppress leakage via placeholder definitions \(def answer := sorry\)\. Measuring Multiple Sorries closes this loophole: the rate stays under2\.5%2\.5\\text\{\\,\}\\mathrm\{\\%\}across all methods \(1\.1%1\.1\\text\{\\,\}\\mathrm\{\\%\}forSage\)\. Thus,Sagegames neither escape hatch, choosing the trilemma’s third option—existential translation—whereasMonolithic\+Semantic’s higher score reflects a higher guessing rate rewarded by the judge\.

An appendix reject audit \([Table11](https://arxiv.org/html/2609.35790#A3.T11)\) shows that both monolithic methods and the fine\-tunedGoedelbaseline failGoedel\-SMmainly via wrong hardcoded answers \(mathematically false / wrong injection\), whereasSageis penalized mainly for open existential encodings—a gap we accept by design, since our in\-loop rater is not tasked with verifying mathematical correctness of injected constants and treats both injection and existential texture as valid\.

Table 7:Structural fidelity onOmni\-MATH\(Answer\-Agnostic, pass@1\)\.MethodCompile\(↑\\uparrow\)Goedel\-SM\(↑\\uparrow\)AnswerLeakage \(%\) \(↓\\downarrow\)MultipleSorries \(%\) \(↓\\downarrow\)Monolithic73\.051\.072\.60\.5Monolithic\+Semantic95\.757\.070\.91\.0Decomposed62\.045\.31\.02\.2Decomposed\+Semantic\(Sage\)94\.754\.02\.71\.1Goedel\(Finetuned\)74\.032\.056\.22\.3Takeaway\.On interrogative benchmarks, standard semantic metrics yield illusory rigor by rewarding unverified answer guessing over faithful mathematical translation\. Evaluating genuine answer\-agnostic formalization requires strict structural audits against leakage and stubbing, as confirmed by our reject analysis \([Table11](https://arxiv.org/html/2609.35790#A3.T11)\) and detailed in[SectionC\.5](https://arxiv.org/html/2609.35790#A3.SS5)\.

## 7Discussion and Limitations

The Autoformalizer as Translator, Not SolverAutoformalizers must act strictly as epistemic translators—faithfully encoding informal mathematical intent into formal logic—rather than solution\-guessing oracles\. Enforcing benchmark discipline requires establishing in advance whether a setting is*Answer\-Aware*or*Answer\-Agnostic*\. When informal proofs are supplied, systems can construct closed, instantiated theorems; when withheld, autoformalizersmust not guess constants, formalizing queries as existential propositions \(∃x,P⁡\(x\)\\exists x,P\(x\)\) or open parameter specifications\. Guessing answers creates an illusion of capability and poisons prover training data: unconstrained monolithic models yield mathematically false targets in80\.6%80\.6\\text\{\\,\}\\mathrm\{\\%\}of rejected cases \(Monolithic\+Semanticreject audit,N=129N=129\)\. Respecting this boundary enablesSageto suppress answer leakage to2\.7%2\.7\\text\{\\,\}\\mathrm\{\\%\}, ensuring mathematically sound formal targets\.

Limitation: Statement Vulnerability in Type TheoryFormalizing open queries as existentials preserves translation fidelity but exposes a key limitation: Lean 4 verifies known assertions rather than governing open discovery\. In classical logic, casting queries intoPropleaves statements vulnerable to shortcuts, as proof irrelevance allows downstream provers to bypass explicit construction via case splits or intensional tautologies\. Fixing this requires going beyond prompt engineering to advanceformalization theory and constructive type theory—specifically, engineering computational target types inTypethat structurally force provers to construct explicit witnesses\.

Limitation: Wall\-Clock Latency and Adaptive VerificationA practical limitation ofSageis wall\-clock latency: coordinating multi\-agent critique with iterative Lean 4 compiler execution requires sequential queries and kernel type\-checks, running slower than unverified single\-pass models\. However, this trade\-off suitscorpus\-scale synthetic data generation—an offline, run\-once curation process where mathematical certification and dataset purity far outweigh millisecond throughput\. Furthermore, our compute footprint is dynamic rather than static: verification intervenes only when syntactic errors or semantic discrepancies are detected, so stronger base generators naturally reduce repair rounds\. As evidenced by our scaling ablation \([Table3](https://arxiv.org/html/2609.35790#S6.T3)\), upgrading the backbone to Qwen3\.8\-27B cuts average repairs to∼\\sim1\.1 while boosting joint fidelity to85\.7%85\.7\\text\{\\,\}\\mathrm\{\\%\}\(98\.0%98\.0\\text\{\\,\}\\mathrm\{\\%\}compilation\), confirming that stronger base models synergize directly with test\-time verification to yield both faster convergence and higher\-fidelity targets\.

## 8Conclusion

Neural theorem proving has reached an inflection point: while proof\-search architectures continue to scale, they remain fundamentally starved of diverse, high\-trust formal statements\. Historically, autoformalization treats this as a purely syntactic challenge, falling prey to an “illusion of rigor” where compilers accept statements that drop hypotheses, alter constraints, or inject false conjectures\.

In this work, we introducedSage, an agentic framework coupling syntactic type\-checking with multi\-dimensional semantic critique to guarantee genuine mathematical fidelity\. By establishing that autoformalizers must operate as faithful translators rather than unconstrained oracles,Sageachieves77\.3%77\.3\\text\{\\,\}\\mathrm\{\\%\}joint fidelity onOmni\-MATHin the answer\-aware regime,73\.3%73\.3\\text\{\\,\}\\mathrm\{\\%\}answer\-agnostic \(at pass@4\), and60\.0%60\.0\\text\{\\,\}\\mathrm\{\\%\}zero\-shot on unformalized International Mathematical Olympiad problems—outperforming fine\-tuned baselines by nearly6×6\\timeswhile suppressing structural answer leakage to2\.7%2\.7\\text\{\\,\}\\mathrm\{\\%\}\.

Ultimately,Sagedemonstrates that inference\-time semantic verification is indispensable for high\-integrity formalization\. By providing a dependable engine for faithful synthetic data generation at scale, our protocol bridges the gap between informal mathematical knowledge and machine\-verifiable truth, laying the groundwork to power the next generation of automated reasoning systems\.

## References

- Ammanamanchiet al\.\(2026\)P\. S\. Ammanamanchi, S\. Bhat, and S\. BidermanFaults in our formal benchmarking: dataset defects and evaluation failures in lean theorem proving\.arXiv preprint arXiv:2606\.29493\.Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- Azerbayevet al\.\(2024a\)Z\. Azerbayev, B\. Piotrowski, H\. Schoelkopf, M\. Dos Santos, and S\. WelleckProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Azerbayevet al\.\(2024b\)Z\. Azerbayev, H\. Schoelkopf, K\. Paster, M\. Dos Santos, S\. McAleer, A\. Q\. Jiang, J\. Deng, S\. Biderman, and S\. WelleckLlemma: an open language model for mathematics\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Chenet al\.\(2026\)G\. Chen, J\. Wu, X\. Chen, W\. X\. Zhao, R\. Song, C\. Li, K\. Fan, D\. Liu, and M\. LiaoReForm: reflective autoformalization with prospective bounded sequence optimization\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- Chenet al\.\(2025\)L\. Chen, J\. Gu, L\. Huang, W\. F\. Huang, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, K\. Ma, P\. Sun, H\. Zhang, and H\. LiSeed\-prover: deep and broad reasoning for automated theorem proving\.arXiv preprint arXiv:2507\.23726\.Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- de Moura and Ullrich \(2021\)L\. de Moura and S\. UllrichThe lean 4 theorem prover and programming language\.InCADE 28,Cited by:[§1](https://arxiv.org/html/2609.35790#S1.p1.1)\.
- Gaoet al\.\(2025\)B\. Gao, F\. Song, Z\. Yang, Z\. Cai, Y\. Miao, Q\. Dong, L\. Li, C\. Ma, L\. Chen, R\. Xu, Z\. Tang, B\. Wang, D\. Zan, S\. Quan, G\. Zhang, L\. Sha, Y\. Zhang, X\. Ren, T\. Liu, and B\. ChangOmni\-MATH: a universal benchmark for mathematics\.InICLR,Cited by:[§C\.1](https://arxiv.org/html/2609.35790#A3.SS1.SSS0.Px1.p1.1),[§5](https://arxiv.org/html/2609.35790#S5.SS0.SSS0.Px1.p1.1)\.
- Gaoet al\.\(2024\)J\. Gao, W\. Zhao, J\. Song, Z\. Shao, H\. Wang, Z\. Z\. Ren, Z\. Fu, Z\. Gou, L\. Zhang, and D\. GuoHerald: a natural language annotated lean benchmark\.arXiv preprint arXiv:2410\.23174\.Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Gouet al\.\(2024\)Z\. Gou, Z\. Shao, Y\. Gong, Y\. Shen, Y\. Yang, N\. Duan, and W\. ChenCRITIC: large language models can self\-correct with tool\-interactive critiquing\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- Honget al\.\(2024\)S\. Hong, M\. Zhuge, J\. Chen, X\. Zheng, Y\. Cheng, C\. Zhang, J\. Wang, Z\. Wang, S\. K\. S\. Yau, Z\. Lin, L\. Zhou, C\. Ran, L\. Xiao, C\. Wu, and J\. SchmidhuberMetaGPT: meta programming for multi\-agent collaborative framework\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- Hubertet al\.\(2025\)T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horvath, G\. Zuzic, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom, D\. Silver, D\. Hassabis, and T\. P\. LillicrapOlympiad\-level formal mathematical reasoning with reinforcement learning\.Nature638,pp\. 740–746\.External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09833-y)Cited by:[§1](https://arxiv.org/html/2609.35790#S1.p1.1),[§2](https://arxiv.org/html/2609.35790#S2.p1.1),[§6\.1](https://arxiv.org/html/2609.35790#S6.SS1.p1.1)\.
- Lampleet al\.\(2022\)G\. Lample, M\. Lachaux, T\. Lavril, X\. Martinet, A\. Hayat, G\. Ebner, A\. Rodriguez, and T\. LacroixHyperTree proof search for neural theorem proving\.InNeurIPS,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- Lightmanet al\.\(2024\)H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. CobbeLet’s verify step by step\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- Linet al\.\(2025\)H\. Lin, S\. Tang, J\. Wu, B\. Lyu, H\. Lin, K\. Yang, J\. Li, M\. Xia, D\. Chen, S\. Arora, and C\. JinGoedel\-Prover\-V2: scaling formal reasoning with natural language feedback\.arXiv preprint arXiv:2508\.03613\.Cited by:[1st item](https://arxiv.org/html/2609.35790#A3.I1.i1.p1.1),[item 3](https://arxiv.org/html/2609.35790#A3.I4.i3.p1.1),[§C\.1](https://arxiv.org/html/2609.35790#A3.SS1.SSS0.Px1.p1.1),[§C\.4](https://arxiv.org/html/2609.35790#A3.SS4.SSS0.Px4.p1.1),[§C\.5](https://arxiv.org/html/2609.35790#A3.SS5.SSS0.Px1.p1.1),[§1](https://arxiv.org/html/2609.35790#S1.p1.1),[§2](https://arxiv.org/html/2609.35790#S2.p1.1),[4th item](https://arxiv.org/html/2609.35790#S5.I2.i4.p1.1),[§5](https://arxiv.org/html/2609.35790#S5.SS0.SSS0.Px1.p1.1),[§5](https://arxiv.org/html/2609.35790#S5.SS0.SSS0.Px2.p1.2),[§6\.1](https://arxiv.org/html/2609.35790#S6.SS1.p1.1)\.
- Liuet al\.\(2023\)C\. Liu, J\. Shen, H\. Xin, Z\. Liu, Y\. Yuan, H\. Wang, W\. Ju, C\. Zheng, Y\. Yin, L\. Li, M\. Zhang, and Q\. LiuFIMO: a challenge formal dataset for automated theorem proving\.arXiv preprint arXiv:2309\.04295\.Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- Liuet al\.\(2025\)Q\. Liu, X\. Zheng, X\. Lu, Q\. Cao, and J\. YanRethinking and improving autoformalization: towards a faithful metric and a dependency retrieval\-based approach\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Luet al\.\(2025\)J\. Lu, Y\. Wan, Y\. Huang, J\. Xiong, Z\. Liu, and Z\. GuoFormalAlign: automated alignment evaluation for autoformalization\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Madaanet al\.\(2023\)A\. Madaan, N\. Tandon, P\. Gupta, S\. Hallinan, L\. Gao, S\. Wiegreffe, U\. Alon, N\. Dziri, S\. Prabhumoye, Y\. Yang, S\. Welleck, B\. P\. Majumder, S\. Gupta, A\. Yazdanbakhsh, and P\. ClarkSelf\-Refine: iterative refinement with self\-feedback\.InNeurIPS,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- Ospanovet al\.\(2025\)A\. Ospanov, F\. Farnia, and R\. YousefzadehminiF2F\-lean revisited: reviewing limitations and charting a path forward\.InNeurIPS,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- Poirouxet al\.\(2025\)A\. Poiroux, G\. Weiss, V\. Kunčak, and A\. BosselutReliable evaluation and benchmarks for statement autoformalization\.InEMNLP,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- Renet al\.\(2025\)Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. RuanDeepSeek\-Prover\-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.arXiv preprint arXiv:2504\.21801\.Cited by:[§1](https://arxiv.org/html/2609.35790#S1.p1.1),[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- Renshaw \(2024\)D\. RenshawCompfiles: mathematics competition problems formalized in Lean 4\.Cited by:[1st item](https://arxiv.org/html/2609.35790#A3.I2.i1.p1.1),[§5](https://arxiv.org/html/2609.35790#S5.SS0.SSS0.Px1.p1.1)\.
- Ridniket al\.\(2024\)T\. Ridnik, D\. Kredo, and I\. FriedmanAlphaCodium: from prompt engineering to flow engineering\.arXiv preprint arXiv:2401\.08500\.Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- Shinnet al\.\(2023\)N\. Shinn, F\. Cassano, A\. Gopinath, K\. Narasimhan, and S\. YaoReflexion: language agents with verbal reinforcement learning\.InNeurIPS,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- The mathlib Community \(2020\)The mathlib CommunityThe lean mathematical library\.InCPP,Cited by:[item 3](https://arxiv.org/html/2609.35790#S4.I1.i3.p1.1)\.
- Wanget al\.\(2025\)H\. Wang, R\. Xie, Y\. Wang, G\. Gao, X\. Yu, and B\. DongAria: an agent for retrieval and iterative auto\-formalization via dependency graph\.arXiv preprint arXiv:2510\.04520\.Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Wanget al\.\(2024a\)K\. Wang, H\. Ren, A\. Zhou, Z\. Lu, S\. Luo, W\. Shi, R\. Zhang, L\. Song, M\. Zhan, and H\. LiMathCoder: seamless code integration in LLMs for mathematical problem solving\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Wanget al\.\(2024b\)K\. Wang, H\. Ren, A\. Zhou, Z\. Lu, S\. Luo, W\. Shi, R\. Zhang, L\. Song, M\. Zhan, and H\. LiProcess\-reward\-model\-guided tree search for mathematical reasoning\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- Wanget al\.\(2018\)Q\. Wang, C\. Kaliszyk, and J\. UrbanFirst experiments with neural translation of informal to formal mathematics\.InIntelligent Computer Mathematics \(CICM\),pp\. 255–270\.External Links:[Document](https://dx.doi.org/10.1007/978-3-319-96812-4%5F22)Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Wuet al\.\(2024\)Q\. Wu, G\. Bansal, J\. Zhang, Y\. Wu, B\. Li, E\. Zhu, L\. Jiang, X\. Zhang, S\. Zhang, J\. Liu, A\. H\. Awadallah, R\. W\. White, D\. Burger, and C\. WangAutoGen: enabling next\-gen LLM applications via multi\-agent conversation\.InCOLM,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p3.1)\.
- Wuet al\.\(2022\)Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. SzegedyAutoformalization with large language models\.InNeurIPS,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Yanget al\.\(2023\)K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Wen, L\. Weiss, A\. Anand, T\. Tuli, A\. Blanco\-Ferrer, C\. Kaliszyk, S\. M\. Watt, C\. Szegedy, L\. de Moura, Y\. Ganor, and A\. KanodiaLeanDojo: theorem proving with retrieval\-augmented language models\.InNeurIPS,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- Yinget al\.\(2024\)H\. Ying, Z\. Shao, Z\. Fu, Z\. Gou, H\. Wang, Z\. F\. Wang, Z\. Z\. Ren, L\. Zhang, D\. Guo, J\. Song, and C\. RuanLean workbook: a large\-scale formal problem set for theorem proving\.arXiv preprint arXiv:2406\.03847\.Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p2.1)\.
- Zhenget al\.\(2022\)K\. Zheng, J\. M\. Han, and S\. PoluminiF2F: a cross\-system benchmark for formal theorem proving\.InICLR,Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.
- Zhouet al\.\(2025\)Y\. Zhou, J\. Zhao, Y\. Zhang, B\. Wang, S\. Wang, L\. Chen, J\. Wang, H\. Chen, A\. Jie, X\. Zhang, H\. Wang, L\. Trung, R\. Ye, P\. N\. Hoang, H\. Zhang, P\. Sun, and H\. LiSolving formal math problems by decomposition and iterative reflection\.arXiv preprint arXiv:2507\.15225\.Cited by:[§2](https://arxiv.org/html/2609.35790#S2.p1.1)\.

## Appendix ATheoretical Foundations, The Feasibility Trilemma, and Type\-Theoretic Locks

The theoretical challenges of autoformalization discussed in[Section3](https://arxiv.org/html/2609.35790#S3)—specifically the Polarity Commitment Problem, the fragility of Existential Encodings, and the Discovery vs\. Verification Gap—are symptoms of a fundamental structural mismatch between natural language mathematical practice and dependent type theory\. In this section, we establish the theoretical foundations of theInterrogative\-Declarative Mismatch, formalize the trade\-offs of theFeasibility Trilemma, dissect the primary syntactic exploits available to downstream provers, and detail the mathematical and constructive implementation ofType\-Theoretic Locksin Lean 4\.

### A\.1The Discovery vs\. Verification Gap and The Law of Syntactic Trivialization

Interactive theorem provers \(ITPs\) like Lean 4, Isabelle/HOL, and Coq are fundamentally designed as*verification engines*\. Given an explicit, pre\-determined propositionP:PropP:\\mathrm\{Prop\}, the system’s role is to verify whether a user\- or tactic\-supplied proof termppwitnesses the validity ofPP\(i\.e\.,p:Pp:P\)\. The specification of the theorem remains fixed and closed prior to the initiation of the proof search\.

In contrast, human mathematical activity and natural language competition benchmarks heavily feature*discovery problems*\. These queries do not supply a closed proposition to verify, but instead pose open interrogative problems asking the reasoner to explore an unbounded search space to discover an unknown mathematical entity:

- •Value Determination:“Compute the remainder when220262^\{2026\}is divided by10001000\.”
- •Witness Construction:“Does there exist a continuous functionf:ℝ→ℝf:\\mathbb\{R\}\\to\\mathbb\{R\}such thatf⁡\(f⁡\(x\)\)=−xf\(f\(x\)\)=\-x?”
- •Full Characterization:“Determine all pairs of integers\(x,y\)\(x,y\)such thatx3\+y3=\(x\+y\)2x^\{3\}\+y^\{3\}=\(x\+y\)^\{2\}\.”
- •Extremal Optimization:“Find the maximum possible area of a convex polygon satisfying…”

When an autoformalization pipeline attempts to translate these discovery queries into an interactive theorem prover, it confronts the tension between two distinct modes of defining mathematical objects:

- •Intensional Definition:Defining a collection or entity strictly by the properties or constraints that its members must satisfy: Sint≜\{x∈𝒳∣P⁡\(x\)\}S\_\{\\mathrm\{int\}\}\\triangleq\\\{x\\in\\mathcal\{X\}\\mid P\(x\)\\\}
- •Extensional Definition:Defining a collection by explicitly evaluating, constructing, and enumerating its concrete elements: Sext≜\{v1,v2,…,vk\}S\_\{\\mathrm\{ext\}\}\\triangleq\\\{v\_\{1\},v\_\{2\},\\dots,v\_\{k\}\\\}

In natural language mathematics, solving a characterization problem requires transitioning from an intensional specification \(P⁡\(x\)P\(x\)\) to an extensional realization \(SextS\_\{\\mathrm\{ext\}\}\), demonstrating that the computed set of witnesses exactly coincides with the predicate’s truth domain\. However, because formal theorem provers evaluate syntactic validity rather than semantic computational effort, formalizing a discovery query as an existential statement over a predicate\-supporting container enables automated provers to bypass the mathematical reasoning entirely\. We formalize this phenomenon as:

> The Law of Syntactic Trivialization:*An automated theorem prover can trivially solve any open\-ended discovery query if the target formal container admits an intensional definition\.*

Whenever the target type allows existence of a set using the comprehension axiom \(such asSetα≡α→Prop\\alpha\\equiv\\alpha\\to\\text\{Prop\}\), an automated solver can simply package the question’s defining predicate back as the solution witness\. The kernel evaluates this identity tautologically \(P⁡\(x\)⇔P⁡\(x\)P\(x\)\\iff P\(x\)\), yielding a fully verified formal proof without computing or discovering any mathematical content\.

### A\.2The Feasibility Trilemma

To translate an open\-ended natural language querySNLS\_\{\\mathrm\{NL\}\}into a formal specificationSFS\_\{\\mathrm\{F\}\}, an autoformalization engine must map the interrogative text into a compilable Lean 4 target\. We identify three distinct formalization paradigms, each imposing unavoidable trade\-offs across syntactic validity, semantic fidelity, pragmatic texture, and oracle dependence:

##### 1\. Explicit Answer Injection\.

The formalizer resolves the unknown value upfront and hardcodes the solution directly into the theorem statement, transforming the open query into a concrete declarative verification claim \(e\.g\., rewriting“Findxxsuch thatx\+5=0x\+5=0”intotheorem target : \(\-5 : Int\) \+ 5 = 0\)\.

- •Advantages:Yields fully closed, highly specified theorems that downstream neural provers can consume directly without modifying the statement structure or touching definitions\.
- •Disadvantages:Completely destroys the pragmatic texture of the query, altering the task from discovery to verification\. Crucially, it requires an external mathematical oracle \(e\.g\., an accompanying informal proofPNLP\_\{\\mathrm\{NL\}\}or a ground\-truth key\) to supply the correct answer prior to formalization\. In zero\-shot settings, any hallucination in the injected answer produces a mathematically false, unprovable theorem\.

##### 2\. Placeholder Definitions\.

The formalizer introduces an unresolved, typed constant via a preliminary definition stubbed with a placeholder, and formulates the primary theorem relative to this placeholder \(e\.g\.,def answer : Int := sorry, followed bytheorem target : answer \+ 5 = 0\)\.

- •Advantages:Preserves the open texture of the query without requiring an oracle; can be generated reliably in zero\-shot, answer\-agnostic settings\.
- •Disadvantages:Violates the fundamental verification boundary of automated theorem proving\. Downstream provers \(such as AlphaProof or Goedel\-Prover\) operate under a strict read\-only contract: they search for a proof term insideby \.\.\.while the theorem declaration and all preceding definitions remain immutable\. Requiring the prover to edit the definition ofanswertransforms the task into code modification rather than tactic proof search, breaking automated evaluation harnesses\.

##### 3\. Existential Encodings\.

The formalizer expresses the open query as an existential proposition over the problem’s constraints \(e\.g\.,theorem target :∃\\existsx : Int, x \+ 5 = 0\), assigning the responsibility of constructing the witness to the proving agent\.

- •Advantages:Retains the literal semantic structure of the informal prompt without requiring an oracle; maintains the immutability of the theorem statement\.
- •Disadvantages:Highly fragile and vulnerable to logical shortcuts\. When applied to binary polar queries, it forces premature commitments or disjunctive tautologies\. When applied to full characterizations, it is immediately vulnerable to the Triviality Trap\.

We synthesize these operational boundaries into:

> *An answer\-agnostic autoformalizer cannot map an open interrogative query into a single declarative proposition without assuming an oracle, breaking downstream prover immutability, or introducing logical vulnerabilities\.*

### A\.3Vulnerabilities of Existential Targets: Polarity and Triviality

When open interrogative queries are encoded as standard propositions in Lean’s propositional universe \(Prop\), downstream automated provers frequently exploit the Interrogative\-Declarative Mismatch through two primary structural vulnerabilities:

##### 1\. The Polarity Cheat\.

Binary \(Yes/No\) questions require determining the truth value of an underlying proposition:“Does there exist an integernnsuch thatP⁡\(n\)P\(n\)holds?”An answer\-agnostic formalizer does not know whether the answer is affirmative or negative:

- •If it commits to a positive existential claim, such astheorem target :∃\\existsn :ℤ\\mathbb\{Z\}, P n, and the mathematical answer is “No”, the formal statement is false and impossible to prove\.
- •If it attempts to maintain neutrality by encoding the query as an open disjunction: theoremtarget\_polar:\(∃\\exists\(n:ℤ\\mathbb\{Z\}\),Pn\)∨\\vee¬\\neg\(∃\\exists\(n:ℤ\\mathbb\{Z\}\),Pn\):=by \-\-ProverexploitstheLawofExcludedMiddle: exactClassical\.em\_\\\_ an automated prover will instantly close the goal in one step using the Law of Excluded Middle\. The prover receives credit for a complete formal proof without ever determining which branch is mathematically true\.

##### 2\. The Triviality Trap\.

Characterization queries ask to“Determine all objectsxxsatisfying propertyP⁡\(x\)P\(x\)\.”When formalized naively inProp, the target asserts the existence of a solution set:

theoremtarget\_characterization:∃\\exists\(S:Setα\\alpha\),∀\\forall\(x:α\\alpha\),x∈\\inS↔\\leftrightarrowPx:=by

\-\-One\-lineautomatedcheatbypassingallmathematicalwork:

use\{x:α\\alpha\|Px\}

introx

rfl

BecauseSetα\\alphais definitionally equal to the predicate typeα→Prop\\alpha\\to\\mathrm\{Prop\}in Lean 4, the set\-builder notation\{x \| P x\}is an intensional syntactic identity\. The type checker accepts this proof trivially becauseP⁡\(x\)⇔P⁡\(x\)P\(x\)\\iff P\(x\)is reflexive\. The automated agent has computed nothing, bypassed all algebraic deductions, and generated an uninformative tautology\.

### A\.4The Defense Matrix: Type\-Theoretic Locks

To definitively safeguard benchmarks against both the Polarity Cheat and the Triviality Trap, we developType\-Theoretic Locks\. The core theoretical mechanism shifts the formal target out of the propositional universe \(Prop\) and into the universe of data types \(Type\) using Lean 4Subtypes:

\{x:α/⁣/P⁡\(x\)\}\\\{x:\\alpha\\mathbin\{/\\mkern\-6\.0mu/\}P\(x\)\\\}A term of this subtype consists of a dependent pair⟨w,h⟩\\langle w,h\\rangle, wherew:αw:\\alphais an explicit computational witness, andh:P⁡\(w\)h:P\(w\)is a formal proof thatwwsatisfies the required constraints\.

##### Defeating the Polarity Cheat \(The Prop\-to\-Type Lock\)\.

By transitioning the target from atheoreminPropto adefinType, we exploit Lean’s fundamental restriction onlarge elimination\. In Lean’s calculus of inductive constructions, a term of a propositionP:PropP:\\mathrm\{Prop\}cannot be eliminated to construct a value in a computational data typeT:TypeuT:\\mathrm\{Type\}\_\{u\}, unlessPPis a syntactic subsingleton \(such asFalseor equality\)\.

BecauseClassical\.emproduces a classical proof inProp, any attempt by an automated prover to invokeClassical\.emto synthesize a term of aType\-level subtype triggers an immediate kernel type\-error\. The prover is physically forced to supply the concrete witness inTypefirst, before Lean allows it to satisfy the accompanying proof obligations\.

##### Defeating the Triviality Trap \(The Constructor Restriction Lock\)\.

To prevent the set\-builder comprehension exploit \(use \{x \| P x\}\), we restrict the target container from the intensionalSetα\\alphato a type such asListα\\alphaorFinsetα\\alpha\.

In Lean’s type theory,Setα\\alphais merely syntactical notation for non\-computational predicate functionsα→Prop\\alpha\\to\\mathrm\{Prop\}\. In contrast,Listα\\alphais an inductive data structure generated strictly by its two constructors,nil\(\[\]\) andcons\(x :: xs\)\. Because Lean’s elaborator cannot definitionally unify an arbitrary logical predicate with an inductive data term, attempting to supply\{x \| P x\}causes an immediate unification failure during elaboration\. To satisfy the type checker, the prover is forced to construct a computational, finite collection directly rather than relying on an unbounded predicate\.

### A\.5Cleaned and Homogenized Lean 4 Lock Implementations

To facilitate adoption in future autoformalization benchmarks, we provide production\-ready, standardized Lean 4 templates implementing Type\-Theoretic Locks across characterization queries, polar decisions, and multiple\-choice questions \(MCQs\)\. All variable names, type annotations, and structural patterns are fully homogenized\.

#### A\.5\.1Characterization Query: Intensional vs\. Extensional Lock

Consider the problem:“Determine all real numbersxxsuch thatx2−4=0x^\{2\}\-4=0\.”

##### Vulnerable Formulation \(IntensionalSetinProp\):

importMathlib

\-\-Vulnerablecharacterizationtarget\(Prop\+intensionalSetofreals\)\.

\-\-Downstreamautomatedproverscanexploitthiswithoutcomputingtheroots\.

theoremvulnerable\_roots\_query:

∃\\exists\(solution\_set:Setℝ\\mathbb\{R\}\),∀\\forall\(x:ℝ\\mathbb\{R\}\),x∈\\insolution\_set↔\\leftrightarrowx2x^\{2\}\-4=0:=by

\-\-EXPLOIT:Proversimplyechoesthequestionpredicateback:

use\{x:ℝ\\mathbb\{R\}\|x2x^\{2\}\-4=0\}

introx

rfl\-\-Closedinstantly\!Zeromathematicalreasoningperformed\.

##### Locked Formulation \(ExtensionalListSubtype inType\):

importMathlib

\-\-Lockedcharacterizationtarget\(Type\+extensionalListofreals\)\.

\-\-Theproverisforcedtoevaluateandsupplytheconcreteroots\[2,\-2\]\.

deflocked\_roots\_query:

\{roots:Listℝ\\mathbb\{R\}/⁣/\\mathbin\{/\\mkern\-6\.0mu/\}roots\.Nodup∧\\wedge∀\\forall\(x:ℝ\\mathbb\{R\}\),x∈\\inroots↔\\leftrightarrowx2x^\{2\}\-4=0\}:=by

\-\-TheproverMUSTsupplytheconcretemathematicalwitnessupfront:

refine⟨\[2,−2\],?​\_⟩\\langle\[2,\-2\],?\\\_\\rangle

\-\-Onlyafterprovidingthewitnessdoestheproverdischargetheverificationobligations:

sorry

#### A\.5\.2Binary Polar Decision: Vulnerable Disjunction vs\. Prop\-to\-Type Lock

Consider the problem:“Is there an integernnsuch thatn2\+1=0n^\{2\}\+1=0?”

##### Vulnerable Formulation \(Disjunction inProp\):

importMathlib

\-\-Vulnerablebinarypolartarget\.

\-\-DownstreamproverscanexploitLEMtobypassdecidingpolarity\.

theoremvulnerable\_polar\_query:

\(∃\\exists\(n:ℤ\\mathbb\{Z\}\),n2n^\{2\}\+1=0\)∨\\vee¬\\neg\(∃\\exists\(n:ℤ\\mathbb\{Z\}\),n2n^\{2\}\+1=0\):=by

\-\-EXPLOIT:Closedinonestepbyclassicallogicwithoutdeterminingtheanswer:

exactClassical\.em\_\\\_

##### Locked Formulation \(Propositional Subtype inType\):

importMathlib

\-\-LockedbinarypolartargetinType\.

\-\-Theprovermustselectthetruepropositionfrom\[P,notP\]beforeprovingit\.

deflocked\_polar\_query\(P:Prop\):

\{selected\_verdict:Prop/⁣/\\mathbin\{/\\mkern\-6\.0mu/\}selected\_verdict∈\\in\[P,¬\\negP\]∧\\wedgeselected\_verdict\}:=by

\-\-Theproverislockedintocommittingtothecorrectpolarityfirst:

refine⟨¬P,?​\_⟩\\langle\\neg P,?\\\_\\rangle

sorry

#### A\.5\.3Standardized Multiple\-Choice Question \(MCQ\) Patterns

Multiple\-choice exams \(e\.g\., AMC, MMLU, JEE\) are ubiquitous in AI evaluation\. Naively translating MCQs as disjoint theorems or propositional disjunctions re\-opens the door to classical shortcuts\. Below, we provide standardized, production\-ready Type\-Lock patterns for the three standard MCQ formats\.

##### 1\. Single\-Select Polar MCQ \(“Which statement is TRUE?”\):

The prover must select the uniquely true proposition among candidate optionsPA,PB,PC,PDP\_\{A\},P\_\{B\},P\_\{C\},P\_\{D\}and provide its mathematical proof\.

importMathlib

\-\-LockedSingle\-SelectPolarMCQtarget\.

\-\-Forcestheprovertoinstantiatechosen\_optionwiththetrueproposition\.

defmcq\_single\_select\_target\(P\_AP\_BP\_CP\_D:Prop\):

\{chosen\_option:Prop/⁣/\\mathbin\{/\\mkern\-6\.0mu/\}chosen\_option∈\\in\[P\_A,P\_B,P\_C,P\_D\]∧\\wedgechosen\_option\}:=by

\-\-Exampleprovercommitment:SelectingoptionC

refine⟨PC,?​\_⟩\\langle P\_\{C\},?\\\_\\rangle

sorry

##### 2\. Multi\-Select MCQ \(“Select All That Apply”\):

The prover must identify the exact sublist of true propositions, while simultaneously proving that every unselected candidate option is strictly false\.

importMathlib

\-\-LockedMulti\-SelectMCQtarget\("SelectAllThatApply"\)\.

\-\-Forcestheprovertosupplytheexactlistoftrueoptionsandrefuteallothers\.

defmcq\_multi\_select\_target\(candidates:ListProp\):

\{selected\_options:ListProp/⁣/\\mathbin\{/\\mkern\-6\.0mu/\}

selected\_options⊆\\subseteqcandidates∧\\wedge

\(∀\\forallp∈\\inselected\_options,p\)∧\\wedge

\(∀\\forallp∈\\incandidates,p∉\\notinselected\_options→\\rightarrow¬\\negp\)\}:=by

\-\-Exampleprovercommitment:SelectingoptionsAandCastheonlytruestatements

refine⟨\[PA,PC\],?​\_⟩\\langle\[P\_\{A\},P\_\{C\}\],?\\\_\\rangle

sorry

##### 3\. Extremal / Optimization MCQ \(“Which candidate set or value is optimal?”\):

The prover must select the optimal mathematical object \(e\.g\., minimal bounding set or maximal value\) from candidate set optionsSA,SB,SC,SDS\_\{A\},S\_\{B\},S\_\{C\},S\_\{D\}according to a propertyPP, and prove that all other valid candidate options are sub\-optimal\.

importMathlib

\-\-LockedOptimization/ExtremalMCQtarget\.

\-\-Forcestheprovertoselectthewinningsetandproveitsoptimality\.

defmcq\_optimization\_target

\(candidates:List\(Setℝ\\mathbb\{R\}\)\)

\(is\_valid:Setℝ\\mathbb\{R\}→\\rightarrowProp\):

\{optimal\_choice:Setℝ\\mathbb\{R\}/⁣/\\mathbin\{/\\mkern\-6\.0mu/\}

optimal\_choice∈\\incandidates∧\\wedge

is\_validoptimal\_choice∧\\wedge

\(∀\\forallS∈\\incandidates,is\_validS→\\rightarrowoptimal\_choice⊆\\subseteqS\)\}:=by

\-\-Exampleprovercommitment:SelectingcandidateoptionA

refine⟨SA,?​\_⟩\\langle S\_\{A\},?\\\_\\rangle

sorry

## Appendix BPipeline Architecture and Decomposed Generation Protocol

In this section, we provide the complete architectural specifications, operational contracts, and execution protocols for theSageframework\. We detail the four\-stage decomposed generation chain, explain the syntax\-only ablation loop and the dual\-signal semantic correction loop, and present a complete step\-by\-step walkthrough on a representative olympiad problem\.

### B\.1Decomposition Protocol and Agent Contracts

Monolithic autoformalization architectures attempt to translate complex natural language statements into fully typed, compilable Lean 4 files in a single unconstrained forward pass\. As established in[Section3](https://arxiv.org/html/2609.35790#S3), this monolithic approach conflates multiple distinct cognitive tasks: domain classification, implicit constraint disambiguation, answer resolution, algebraic abstraction, and low\-level Lean syntax formatting\. This coupling makes error localization impossible and frequently leads to severe answer leakage in zero\-shot settings\.

To enforce strict modular boundaries and ensure complete transparency,Sagedecomposes the generation process into four role\-isolated agents \(Distiller, Preprocessor, Formalizer, and Formatter\), summarized in[Table8](https://arxiv.org/html/2609.35790#A2.T8)\.

##### 1\. The Distiller\.

EvaluatesSNLS\_\{\\mathrm\{NL\}\}and informal proofPNLP\_\{\\mathrm\{NL\}\}\(when available\)\. In the answer\-aware regime, it classifies the problem type \(Assertion\- vs\. Question\-type\) and extracts the target witness or characterization from the proof as an Inferred Goal; in the answer\-agnostic regime, it reformulates open interrogative queries into explicit declarative targets without an answer oracle:

- •Mathematical Domain Identification:The agent categorizes the problem into its primary mathematical discipline \(e\.g\., Number Theory, Real Analysis, Combinatorics, Abstract Algebra, Euclidean Geometry\)\. This classification primes downstream retrieval and informs Mathlib namespace scoping\.
- •Answer\-Aware Regime \(With\-Proof\):When an informal proofPNLP\_\{\\mathrm\{NL\}\}is supplied as an oracle, the Distiller analyzes the logical resolution of the problem\. For Assertion\-type problems \(e\.g\., “Prove that…”\), the claim is self\-contained and the Inferred Goal \(Inferred Goal\) remains empty\. For Question\-type problems \(e\.g\., “Find all…”, “Determine the value of…”\), the Distiller extracts the definitive mathematical witness, numeric constant, or characterization established byPNLP\_\{\\mathrm\{NL\}\}as the Inferred Goal\.
- •Answer\-Agnostic Regime \(Without\-Proof\):When no proof is provided, the Distiller is strictly forbidden from computing or hallucinating answers\. Instead, it reformulates the open query into an unambiguous declarative proposition using existential \(∃\\exists\), unique existential \(∃\!\\exists\!\), or extremal quantification, leaving the constructive witness search entirely to downstream provers\.

##### 2\. The Preprocessor\.

The Preprocessor converts the distilled problem into a structured Declarative Normal Form representation \(SDNFS\_\{\\mathrm\{DNF\}\}\) and decomposes it into symbolic components across four strict sequential phases:

- •Phase 0 \(SDNFS\_\{\\mathrm\{DNF\}\}Generation\):If the Inferred Goal is empty,SDNFS\_\{\\mathrm\{DNF\}\}matchesSNLS\_\{\\mathrm\{NL\}\}\. If the Inferred Goal is non\-empty, the agent constructs a declarative natural language assertion stating that the Inferred Goal uniquely satisfies the problem’s conditions\.
- •Phase 1 \(Assertion Extraction\):Isolates the primary mathematical claim as the final symbolic goalGG\.
- •Phase 2 \(Global Infrastructure\):Identifies supporting mathematical objects, relations, or functions, specifying them as structured signatures: def \[Name\] \(inputs : Type\) : \[Output Type\] := \[Formula\]
- •Phase 3 \(Hypothesis Extraction\):Isolates all antecedent conditions, bounds, and premises into a numbered roster:h1,…,hnh\_\{1\},\\dots,h\_\{n\}, where eachhih\_\{i\}is paired with a concise mathematical description\.

##### 3\. The Formalizer\.

The Formalizer maps the preprocessed pseudocode blocks into idiomatic, fully typed Lean 4 signatures\. Guided by an*Anti\-Trivialization Guard*, it enforces the following protocol:

- •Definitions Block:Each auxiliary construct extracted in Phase 2 is translated into a standalone, well\-typed Lean 4def\. The agent searchesMathlibfor standard constructions to ensure modularity and idiomatic typing\.
- •Theorem Signature:The agent constructs the primary theorem declaration by binding all hypotheses and asserting the target goal fori∈\{1,⋯,n\}i\\in\\\{1,\\cdots,n\\\}: theorem \[name\] \(h\_i : \[translated\_i\]\) : \[G\] := by sorryWhere an informal condition lacks a directMathlibprimitive, the Formalizer establishes a dedicated predicate definition prior to the theorem: def \[prop\_name\] \(\[args\]\) : Prop := \[definition\]and instantiates it inside the theorem header via\(h : \[prop\_name\] \[args\]\)\. The signature terminates immediately at:= by sorry\.

##### 4\. The Formatter\.

The Formatter acts as the final syntactic integrator\. Because language models frequently output surrounding conversational commentary, omit necessary imports, misplace namespaces, or generate unalignednoncomputable sectiontags, the Formatter cleans and normalizes the code\. Its operational rules mandate: \(i\) insertingimport Mathliband required module headers, \(ii\) managing namespace opens, \(iii\) stripping all conversational natural language, and \(iv\) preserving every mathematical definition and theorem signature verbatim without modifying the underlying formal semantics\.

Table 8:Sagegeneration pipeline\.The sequential, role\-isolated agents composing the generation chain\. Each stage processes specialized mathematical components, ensuring clear translation contracts before generating the final compilable Lean 4 code\.AgentInputOutputDescription & Core RoleDistillerSNLS\_\{\\mathrm\{NL\}\},PNLP\_\{\\mathrm\{NL\}\}?Domain \+ Inferred Goal contextIdentifies the mathematical domain and either extracts the Inferred Goal from the proof or reformulates the open query into a declarative statement\.PreprocessorDistiller outputSDNFS\_\{\\mathrm\{DNF\}\}, local defs, hyps,GGStandardizes the problem into a unified Declarative Normal Form Statement statement \(SDNFS\_\{\\mathrm\{DNF\}\}\) and decomposes it into assumptions, local definitions, and goals\.FormalizerSDNFS\_\{\\mathrm\{DNF\}\}componentsLeandefs \+theorem … sorryMaps assumptions and infrastructure into idiomatic Lean 4 statements, relying onMathlibconcepts while avoiding trivialization\.FormatterDraft codeStandalone\.leanfileOrganizes namespaces, imports, and scaffolding into a compilable file without altering the underlying mathematical meaning\.

### B\.2Correction Loop Protocol

After the generation chain \(decomposed or monolithic\) produces an initial candidate statement, every multi\-round variant enters the same iterative refinement skeleton for up toTTrounds\. Each round evaluates the current candidate under the loop’s exit gate; if the gate fails and the round budget remains, a Corrector receives a structured briefing, emits a revised standalone Lean 4 file, and the candidate is re\-verified\. All Correctors share a fixed output contract: emit a complete Lean 4 file beginning withimport Mathlib; terminate the main claim at:= by sorry\(or preserve an existingproof\_wantedform\); and forbid proof tactics, helper lemmas,admit, or solving the underlying mathematics\. The two instantiations below differ only in the exit gate and in which signals populate the Corrector briefing\.

Both the syntax\-only and dual\-signal loops share two mechanisms that stabilize iterative repair:

##### Syntactic Error De\-cascading\.

In Lean 4, compiler diagnostics frequently suffer from extreme cascading: an early typo or minor type error in an initial definition can trigger dozens of downstream errors throughout the theorem header\. Supplying an uncurated stream of 30\+ compiler errors overwhelms language models, inducing destructive over\-correction on otherwise sound code\. To stabilize repair, the Lean Verifier extracts the firstkkcompiler errors to retain context, but explicitly instructs the Corrector to prioritize resolving the very first error \(e1e\_\{1\}\)\. This top\-down stabilization prevents chaotic thrashing across iterations\.

##### Oscillation Mitigation via Prior Failed Attempts\.

Iterative repair loops can suffer from cyclic oscillation, where the model alternates between two conflicting fixes across successive rounds\. To prevent this, the Corrector briefing dynamically maintains a*Prior Failed Attempts*history log containing the statements attempted in previous rounds and their failure reasons\. This history acts as a negative memory constraint, forcing the Corrector to explore alternative Mathlib abstractions rather than repeating previously rejected patterns\.

### B\.3Syntax\-Only Repair Loop

The ablation variantsDecomposed\+SyntaxandMonolithic\+Syntaxisolate the contribution of compiler feedback without semantic gating\. After the same initial draft as their single\-pass counterparts \(decomposed or monolithic\), they enter the shared repair skeleton above for up toTTrounds\. A dedicated syntax Corrector receives the informal statement, the current Lean draft, and the verifier report then emits a revised signature file under the shared Corrector contract\. The loop exits successfully as soon asCompileholds, or when the round budgetTTis exhausted\. Because termination depends solely on type\-checking, a candidate may leave the loop as a compiling but mathematically unfaithful statement—the failure mode measured when comparing syntax\-only rows toSagein[Section6](https://arxiv.org/html/2609.35790#S6)\.

### B\.4Dual\-Signal Semantic Correction Loop

When the initial draft is executed in the Lean 4 environment,Sageevaluates it with both an objective compiler check and the in\-loop semantic Rater\. A candidate exits successfully only when the joint gateCompile∧\\wedgeSage\-SMis satisfied; otherwise the Corrector is invoked for up toTTrounds under the shared skeleton above\. In standard compile\-only repair, an Large Language Model often restores well\-typedness by deleting or trivializing hypotheses, destroying the intended meaning\. To prevent this, the Corrector receives a structured bipartite diagnosis at every round:

1. 1\.Syntactic feedback:The firstkkcompiler error diagnostics \(line, column, and message\) from the Lean 4 verifier\.
2. 2\.Semantic feedback:Failing dimensions, scores, rationales, and localized mismatch snippets from the in\-loopRater, together with a Rater\-proposed repair draft\.

The Corrector is instructed to prioritize*semantic match over compilation*: a syntactically flawed but semantically faithful draft is treated as a productive intermediate state, whereas a compiling but mathematically incorrect statement must not be preserved\. The loop terminates successfully only whenCompile∧\\wedgeSage\-SMholds\.

##### Pre\-compilation of Semantic Drafts\.

During semantic evaluation, the Rater scores the candidate statement across the different gating dimensions and proposes an alternative draft designed to repair identified semantic mismatches\. Instead of naively passing this draft to the Corrector,Sagefirst compiles the Rater’s draft in Lean 4\. When the Corrector is invoked, it receives a synchronized bipartite diagnosis:

1. 1\.The compilation status and exact compiler diagnostics of its own previous attempt\.
2. 2\.The Rater’s multidimensional semantic critique, the Rater’s proposed draft, and the verified compilation status of that proposed draft\.

This mechanism prevents the Corrector from blindly adopting drafts that fix semantics but break syntax, forcing it to synthesize a solution that simultaneously satisfies both Lean’s type checker and the semantic intent of the original mathematical query\.

##### Anti\-Solver and Anti\-Injection Guard\.

In zero\-shot and answer\-agnostic settings, a naive rater may occasionally suggest “fixing” an existential goal by calculating the numerical answer and setting the variable to a constant or placeholder \(e\.g\., suggesting=42=42or an uninstantiated constantXX\)\. To protect benchmark integrity, the Corrector is governed by a strict*Anti\-Solver Rule*and an*Anti\-Injection Escape Clause*\. The agent is explicitly forbidden from performing calculations, solving the mathematical problem, or injecting concrete witnesses to silence type errors\. If a proposed rater correction introduces an injected answer or an undefined placeholder, the Corrector is instructed to reject that modification and maintain the open\-ended existential formulation \(e\.g\.,∃\!N,…\\exists\!N,\\dots\)\.

### B\.5Compositional Generation Walkthrough

[Figure4](https://arxiv.org/html/2609.35790#A2.F4)illustrates the complete execution trace of theSagepipeline on problemOmni\-MATH\#043 across both operational regimes:

- •Answer\-Aware Regime \(Guided byPNLP\_\{\\mathrm\{NL\}\}\):The Distiller analyzes the informal proof64=43⇒642=46⇒n=664=4^\{3\}\\Rightarrow 64^\{2\}=4^\{6\}\\Rightarrow n=6and extracts the Inferred Goaln=6n=6\. The Preprocessor generatesSDNFS\_\{\\mathrm\{DNF\}\}:“If4n=6424^\{n\}=64^\{2\}, thenn=6n=6”, binds hypothesish1:4n=642h\_\{1\}\\colon 4^\{n\}=64^\{2\}, and sets goalG:n=6G\\colon n=6\. The Formalizer produces an explicit verification theorem assertingn=6n=6\.
- •Answer\-Agnostic Regime \(Zero\-Shot without Proof\):Deprived of an answer oracle, the Distiller refuses to compute the exponent\. It reformulates the open query into an objective unique existential claim \(∃\!n\\exists\!\\,n\)\. The Preprocessor binds this into goalG:∃\!n,4n=642G\\colon\\exists\!\\,n,\\ 4^\{n\}=64^\{2\}, and the Formalizer generates an existential theorem in Lean 4, delegating the computation ofnnto downstream provers\.

Informal statementSNLS\_\{\\mathrm\{NL\}\}*If4n=6424^\{n\}=64^\{2\}, what is the value ofnn?*Answer\-aware also receivesPNLP\_\{\\mathrm\{NL\}\}:64=43⇒642=46⇒n=664=4^\{3\}\\Rightarrow 64^\{2\}=4^\{6\}\\Rightarrow n=6\.Answer\-Aware \(withPNLP\_\{\\mathrm\{NL\}\}\)Answer\-Agnostic \(no proof\)Distiller •Domain: Algebra•Inferred Goal:n=6n=6Distiller •Domain: Algebra•Declarative reformulation:∃\!n\\exists\!\\,ns\.t\.4n=6424^\{n\}=64^\{2\}Preprocessor •SDNFS\_\{\\mathrm\{DNF\}\}: If4n=6424^\{n\}=64^\{2\}, thenn=6n=6•Hypotheses:h1:4n=642h\_\{1\}\\colon 4^\{n\}=64^\{2\}•Definitions: None•GG:n=6n=6Preprocessor •Adopt declarative reformulation asSDNFS\_\{\\mathrm\{DNF\}\}•Hypotheses: None•Definitions: None•GG:∃\!n,4n=642\\exists\!\\,n,\\ 4^\{n\}=64^\{2\}Formalizer \+ Formatter theorem power\_equation\_solution \(n : Nat\) \(h1 : 4ˆn = 64ˆ2\) : n = 6 := by sorryFormalizer \+ Formatter theorem exists\_unique\_real\_n : ∃\!\\exists\!n : Real, \(4 : Real\)ˆn = \(64\)ˆ2 := by sorry

Figure 4:Compositional generation walkthroughonOmni\-MATH\#043\. The same informal question is processed under both regimes\. WithPNLP\_\{\\mathrm\{NL\}\}, the Distiller extracts an Inferred Goal \(n=6n=6\) and the Preprocessor builds a Declarative Normal Form Statement claim with hypothesish1h\_\{1\}and goalG:n=6G\\colon n=6\. Without a proof, the Distiller commits to a declarative reformulation \(∃\!n\\exists\!\\,n\), which flows through to an existential Lean 4 goal\.

## Appendix CExperimental Setup, Datasets, and Reproducibility

In this section, we provide comprehensive details on the benchmark datasets, the language model serving infrastructure, the evaluated model backbones, our compute environment constraints, and the full configuration matrix across all experimental ablations\.

### C\.1Dataset Details and Curation

To test autoformalization across diverse problem types and formalization regimes, our study evaluates on three benchmarks:Omni\-MATH,IMO\-Formalized, andIMO\-Unformalized\. Both IMO suites are derived from a comprehensive snapshot of the community archive taken in July 2026\.

##### Omni\-MATH\(N=300N=300\)\.

Omni\-MATH\([Gao et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib35)\)is an olympiad\-level competition benchmark spanning contests such as AMC 10/12, AIME, USAMO, and Putnam\. We evaluate on the exact 300\-problem subset benchmarked by Goedel\-Prover\-V2\([Lin et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib28)\)to ensure direct comparability\.

- •Curation Protocol:Extracted directly from the standardized 300\-problem evaluation split of[Lin et al\. \(2025\)](https://arxiv.org/html/2609.35790#bib.bib28)\.
- •Problem Texture:*Question\-type*98\.7%98\.7\\text\{\\,\}\\mathrm\{\\%\};*Assertion\-type*1\.3%1\.3\\text\{\\,\}\\mathrm\{\\%\}\. Question\-type statements require calculating or identifying unknown extremal values, witnesses, or configurations\.
- •Domain Distribution:From the dataset metadata primary subject tags: Algebra \(62\.7%62\.7\\text\{\\,\}\\mathrm\{\\%\}\), Number Theory \(29\.0%29\.0\\text\{\\,\}\\mathrm\{\\%\}\), Combinatorics \(6\.3%6\.3\\text\{\\,\}\\mathrm\{\\%\}\), and Precalculus \(2\.0%2\.0\\text\{\\,\}\\mathrm\{\\%\}\)\. This 300\-subset contains no Geometry\-tagged problems\.

##### IMO\-Formalized\(N=223N=223\)\.

This benchmark comprises all historical International Mathematical Olympiad \(IMO\) problems from 1959 to 2024 that possess official, human\-verified formalizations in Lean 4\.

- •Curation Protocol:Extracted from a snapshot of the[compfiles](https://github.com/dwrensha/compfiles)repository\([Renshaw, 2024](https://arxiv.org/html/2609.35790#bib.bib34)\)taken in July 2026\. It represents the fraction of historical IMO problems \(223/398223/398\) already formalized by the Lean community, with informal statements extracted from module docstrings and formal declarations parsed into standalone targets\.
- •Problem Texture:Nearly balanced:*Question\-type*51\.6%51\.6\\text\{\\,\}\\mathrm\{\\%\};*Assertion\-type*48\.4%48\.4\\text\{\\,\}\\mathrm\{\\%\}\.
- •Domain Distribution:Distiller\-assigned primary domains, mapped to the four canonical IMO disciplines \(analysis / functional\-equation labels folded into Algebra\): Number Theory \(33\.2%33\.2\\text\{\\,\}\\mathrm\{\\%\}\), Algebra \(33\.6%33\.6\\text\{\\,\}\\mathrm\{\\%\}\), Combinatorics \(26\.5%26\.5\\text\{\\,\}\\mathrm\{\\%\}\), and Geometry \(6\.7%6\.7\\text\{\\,\}\\mathrm\{\\%\}\)\.

##### IMO\-Unformalized\(N=175N=175\)\.

This benchmark comprises the complementary frontier of historical IMO problems that have never been formalized in Lean 4\.

- •Curation Protocol:Derived from the same July 2026compfilessnapshot by strictly selecting the complement fraction \(175/398175/398\) that lacked official human formalizations\. Problem texts and informal solution notes were curated from the AI\-MO olympiads compendium and official IMO archives\.
- •Problem Texture:*Assertion\-type*64\.0%64\.0\\text\{\\,\}\\mathrm\{\\%\};*Question\-type*36\.0%36\.0\\text\{\\,\}\\mathrm\{\\%\}\.
- •Domain Distribution:Distiller\-assigned primary domains under the same four\-discipline mapping: Geometry \(69\.1%69\.1\\text\{\\,\}\\mathrm\{\\%\}\), Combinatorics \(24\.6%24\.6\\text\{\\,\}\\mathrm\{\\%\}\), Algebra \(3\.4%3\.4\\text\{\\,\}\\mathrm\{\\%\}\), and Number Theory \(2\.9%2\.9\\text\{\\,\}\\mathrm\{\\%\}\)\. The Geometry skew reflects which historical IMO problems remain unformalized in Lean 4\.

### C\.2LLM Serving, Models, and Infrastructure

All language model inference is executed using the high\-performancevLLMengine\. Each model is served on dedicated GPU instances with a tensor parallelism degree of 1, utilizing FP8 quantized weights and dynamic KV caching to maximize token throughput during iterative multi\-agent correction loops\.

##### Evaluated Models and Pipeline Roles\.

Our experimental framework strictly decouples generation, in\-loop rating, and post\-hoc evaluation to eliminate circular self\-evaluation bias:

1. 1\.Generation & In\-Loop Rating \(Qwen3\.6\-27B\):We deployQwen/Qwen3\.6\-27B\-FP8as the core workhorse model\. It powers all four stages of the generation chain \(Distiller, Preprocessor, Formalizer, Formatter\) as well as the in\-loop semantic Rater and Statement Corrector\.
2. 2\.Independent Post\-Hoc Evaluator \(Gemma4\-31B\):To ensure an unbiased, external evaluation of semantic fidelity, all post\-hoc consensus judging \(Goedel\-SM\) and blind pairwise win\-rate adjudications \(PWR\) are performed usingRedHatAI/gemma\-4\-31B\-it\-FP8\-Dynamic\.
3. 3\.Domain\-Specialized Baseline \(Goedel\-Formalizer\-V2\-32B\):We evaluate againstGoedel\-LM/Goedel\-Formalizer\-V2\-32B\([Lin et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib28)\), an open\-weights model explicitly fine\-tuned for Lean 4 statement autoformalization\.

[Table9](https://arxiv.org/html/2609.35790#A3.T9)details the decoding hyperparameters, sampling bounds, and generation settings across each model role\.

Table 9:LLM decoding and sampling hyperparameters\.Settings are strictly isolated by model role to ensure deterministic evaluation boundaries\.ModelRoleTemp\.Max tokensRetriesQwen3\.6\-27BPipeline generation \+ in\-loop rater0\.616,3842Goedel\-Formalizer\-V2\-32BFine\-tuned baseline \(Goedel\)0\.716,3841Gemma4\-31BPost\-hoc evaluation \(Goedel\-SM/PWR\)0\.616,3842
##### Note on Model Backbones and Qwen 3\.8\.

All primary experiments, benchmark sweeps, and ablation ladders were established using Qwen3\.6\-27B, which served as our stable workhorse throughout development\. Qwen3\.8\-27B was released late in our experimental cycle\. While its enhanced capabilities yield substantial performance gains in our scaling ablation \([Table3](https://arxiv.org/html/2609.35790#S6.T3)\), its extended reasoning traces noticeably increased per\-step latency\. Given the multi\-agent nature and multi\-round repair loops of our pipeline, re\-executing the full experimental suite across all benchmarks was impractical within our project timeline\. We therefore maintain Qwen3\.6\-27B as the consistent backbone across all primary comparative tables\.

##### Compute Environment and Model Access\.

All experiments and evaluations were conducted on an on\-premise computing cluster equipped with dedicated GPU nodes\. To prioritize scientific reproducibility, eliminate dependency on closed commercial APIs with volatile endpoints, and ensure strict data governance, our framework relies exclusively on publicly available, open\-weights models deployed locally\. This setup ensures that all benchmarks, latency profiles, and generated formal artifacts are fully deterministic, auditable, and reproducible by the broader research community without reliance on proprietary black\-box services\.

### C\.3Method Variants and Ablation Configurations

To systematically isolate the individual contributions of pipeline decomposition, syntactic error feedback, and semantic rating feedback, we benchmark six primary configurations across two operational regimes, detailed in[Table10](https://arxiv.org/html/2609.35790#A3.T10)\. For all iterative methods, the maximum repair budget is set toT=5T=5rounds onOmni\-MATHandT=10T=10rounds onIMO\-Unformalized:

- •Single\-Pass Baselines \(T=1T=1\):Monolithicgenerates the formal statement in a single forward pass without intermediate scaffolding\.Decomposedexecutes the four\-stage generation chain \(Distiller, Preprocessor, Formalizer, Formatter\) without entering a correction loop\.
- •Syntax\-Only Loops:Monolithic\+SyntaxandDecomposed\+Syntaxiteratively refine candidate statements using only Lean 4 compiler error diagnostics\.
- •Dual\-Signal Semantic Loops:Monolithic\+SemanticandSage\(Decomposed\+Semantic\) supply the Corrector with both compiler errors and multidimensional in\-loop semantic ratings \(Sage\-SM\)\.

Table 10:Overview of evaluated methods and ablation variants\.We evaluate both monolithic and decomposed variants under matching iteration budgets to systematically isolate the impact of our dual\-signal correction loop\.MethodBase ModelArchitectureFeedback TypeRounds \(TT\)Monolithic ConfigurationsMonolithicQwen3\.6\-27BMonolithicNone1Monolithic\+SyntaxQwen3\.6\-27BMonolithicCompile5–10Monolithic\+SemanticQwen3\.6\-27BMonolithicCompile\+Sage\-SM5–10Decomposed Configurations \(Ours\)DecomposedQwen3\.6\-27BDecomposedNone1Decomposed\+SyntaxQwen3\.6\-27BDecomposedCompile5–10Sage\(Decomposed\+Semantic\)Qwen3\.6\-27BDecomposedCompile\+Sage\-SM5–10External BaselineGoedelGoedel\-Formalizer\-V2\-32BMonolithicNone1

### C\.4Evaluation Metrics and Integrity Audits

Standard autoformalization evaluations typically report raw compilation rates \(Compile\), implicitly assuming that syntactically valid code implies mathematical correctness\. In reality, models frequently generate type\-correct formalizations that are mathematically vacuous, structurally altered, or unfaithful to the informal source\. To establish an honest evaluation standard, our protocol decouples syntactic compilation from post\-hoc semantic validation, and introduces strict automated audits for benchmark integrity\.

##### Compilation Environment \(Compile\)\.

All Lean 4 compilation checks are executed in isolated worker processes managed by our verification engine\. Every candidate file imports Mathlib and is verified against a pinned Lean 4 toolchain\. A formalization passesCompileif the environment returns an exit code of 0 without diagnostic type errors\. Proof bodies are omitted via:= by sorry\. Statements that trigger compiler timeouts \(\>\>30s30\\text\{\\,\}\\mathrm\{s\}\) or memory exhaustion are treated as compilation failures\.

##### The Single\-Sorry Invariant and Cheat Detection\.

As introduced in[Section4\.2](https://arxiv.org/html/2609.35790#S4.SS2), a valid statement must respect thesingle\-sorry contract\. Permitting multiple placeholders exposes benchmarks to two severe vulnerabilities:

1. 1\.*Definition Stubbing:*Models can declare unresolved constant definitions stubbed with a placeholder \(e\.g\.,def k : Nat := sorry\), and subsequently state a trivial theorem overk\. While syntactically valid, any proof over an uninstantiated definition is vacuous\.
2. 2\.*Hypothesis and Lemma Evasion:*Models frequently decompose hard theorems into intermediate helper lemmas closed bysorry\(e\.g\.,lemma helper : \.\.\. := by sorry\), effectively assuming the problem’s deepest mathematical barrier rather than stating a self\-contained target\.

Our audit strips comments and string literals from the Lean source, then counts unresolved placeholder tokens \(sorry,admit,proof\_wanted, and related forms\)\. A prover\-ready candidate must contain exactly one terminating placeholder on the main theorem proof\. Any compiling candidate with more than one placeholder, or with placeholders inside intermediate definitions or helper lemmas, is disqualified as*Multiple Sorries*\.

##### Answer Leakage Audit Protocol\.

When evaluating open\-ended*Question\-type*problems under the answer\-agnostic \(without\-proof\) regime, models are tasked with formalizing the question itself, not computing the solution\. However, monolithic models frequently shortcut the translation by searching for the answer during generation and hardcoding the numeric result into the theorem signature \(e\.g\., translating “Find the minimum value off⁡\(x\)f\(x\)” intotheorem T :∀\\forallx, f x≥\\geq42\)\. We audit this with an independent LLM judge \(Gemma4\-31B\)\. Given the informal statement, the informal proof when available, and the generated Lean code, the auditor runs a fixed protocol:

1. 1\.Texture classification\.Decide whether the informal problem is Assertion\-type \(self\-contained claim\) or Question\-type \(asks to compute, determine, or construct an object\)\. Assertion\-type problems are excluded from leakage penalties, even if their mathematics involves existentials\.
2. 2\.Witness presence\.Check whether the formal statement embeds a concrete witness term or numeric value rather than an open encoding \(e\.g\.,∃\\exists/∃\!\\exists\!\)\.
3. 3\.Match and type check\.If a witness is embedded, check whether it matches the ground\-truth solution and whether its Lean type is compatible with what the informal problem asks for\.

In the answer\-agnostic regime, any compiling Question\-type formalization that embeds a concrete witness is flagged asAnswer Leakage\.

##### Post\-Hoc Consensus Semantic Match \(Goedel\-SM\)\.

For comparability with prior work, we report post\-hoc semantic match under the Goedel\-Prover\-V2 protocol\([Lin et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib28), Appendix D\): an independent Gemma4\-31B judge, queried repeatedly, with success only under unanimous*Appropriate*consensus\. Full consensus settings, prompt\-bias analysis, and reject\-reason taxonomy are in[SectionC\.5](https://arxiv.org/html/2609.35790#A3.SS5)\. Because that judge prefers explicit answer injection, leakage audits are essential when interpreting these scores\.

##### Multi\-Dimensional In\-Loop Semantic Gate \(Sage\-SM\)\.

Unlike a single post\-hoc*Appropriate*/*Not Appropriate*prompt, our in\-loop gate \(Sage\-SM\) evaluates formalizations with the multi\-dimensional Rater from[Section4\.2](https://arxiv.org/html/2609.35790#S4.SS2): Missing, Wrong, Extra, Semantic Match, Exactness, Naturality, and Descriptive Precision\. A candidate passesSage\-SMonly if all seven gated scores clear their configured cutoffs\. The Rater additionally scores auxiliary diagnostic dimensions \(e\.g\., Form Integrity, Compilability, and problem difficulty\); these inform repair suggestions but do not enter the binarySage\-SMdecision\. The gate steers the Statement Corrector during search and can also filter high\-trust training statements post hoc\.

##### Blind Pairwise Win Rate \(PWR\)\.

To evaluate semantic fidelity without rigid prompt heuristics, we perform blind head\-to\-head pairwise comparisons between model outputs𝒜\\mathcal\{A\}andℬ\\mathcal\{B\}\. An independent judge compares both formalizations against the informal source on a 5\-point Likert scale:*Much Worse*\(−2\-2\),*Worse*\(−1\-1\),*Tie*\(00\),*Better*\(\+1\+1\), and*Much Better*\(\+2\+2\)\. To eliminate positional bias, every pair is evaluated twice with swapped presentation orders:\(𝒜,ℬ\)\(\\mathcal\{A\},\\mathcal\{B\}\)and\(ℬ,𝒜\)\(\\mathcal\{B\},\\mathcal\{A\}\)\. Inconsistent orders are reconciled via tie assignment\. We report preference shares over all comparisons \(strict wins, ties, and losses\); conditional on non\-ties, the win rate is the share of decisive comparisons where a method is strictly preferred\.

##### Joint Evaluation Criteria and Sample Aggregation\.

Our primary evaluation metric is the joint criterionCompile∧Goedel\-SM\\textsf\{Compile\}\\wedge\\textsf\{Goedel\-SM\}\{\}, denoting candidate statements that are simultaneously well\-typed in Lean 4 and unanimously approved by the post\-hoc semantic judge\. For multi\-sample search \(pass@​N\\text\{pass@\}N\), a problem is counted as solved under a given metric if*at least one*of theNNindependent candidate generations satisfies the required criteria\.

### C\.5Goedel Evaluation Protocol and Prompt Bias Analysis

##### Consensus Protocol\.

To measure post\-hoc semantic fidelity \(Goedel\-SM\), we adopt the evaluation prompt from Goedel\-Prover\-V2\([Lin et al\., 2025](https://arxiv.org/html/2609.35790#bib.bib28)\), modifying it only to enforce structured JSON parsing\. We deploy Gemma4\-31B as the independent evaluator\. For each candidate statement, we query the judge four independent times\. Each query outputs a categorical verdict of either*Appropriate*or*Not Appropriate*, together with a short free\-form rationale\. Following[Lin et al\. \(2025\)](https://arxiv.org/html/2609.35790#bib.bib28), a formalization is counted as successful underGoedel\-SMif and only if it achieves a unanimous4/44/4*Appropriate*consensus; we leave this decision rule unchanged\.

##### Prompt bias \(from the few\-shot examples\)\.

A qualitative reading of the demonstrations embedded in theGoedel\-SMprompt shows a structural preference for explicit answer injection over open encodings\.

- •For a problem asking for the intercept of a quadratic polynomial, the prompt marks a formalization*Appropriate*because it injects the resolved numeric value \(f 3 = 0\)\.
- •For a problem asking for the equation of a tangent line, the prompt marks an answer\-agnostic formulation*Inappropriate*, on the grounds that “*The translation shifts the problem from deriving the tangent line to verifying a given line equation\.*”

Thus the judge is instructed, by example, to reward closed witnesses and to penalize faithful open formulations that defer the answer\. We do not alter these demonstrations: changing them would change the Goedel protocol itself\.

##### Reject\-reason audit\.

To measure how this bias manifests in practice—without perturbing the judge—we attribute Inappropriate votes*post hoc*by inspecting the returned rationales onOmni\-MATH\(answer\-agnostic, pass@1\)\. We first ask an LLM to propose rejection categories from those rationales, consolidate them into a fixed taxonomy of twenty categories, and then ask Qwen3\.6\-27B to assign every applicable category to each rejection \(multi\-hot\)\.[Table11](https://arxiv.org/html/2609.35790#A3.T11)reports the three most frequent categories\.

Table 11:Goedel\-SM reject reasons onOmni\-MATH\(Answer\-Agnostic\) at pass@1\.Three most common categories among*Inappropriate*samples \(multi\-hot; lower is better\)\. Bold==lowest rate\.MethodNrejectionN\_\{\\mathrm\{rejection\}\}WrongInjection \(%\)MathematicallyFalse \(%\)Existential \(%\)Monolithic14769\.484\.48\.2Monolithic\+Semantic12968\.280\.615\.5Decomposed1648\.522\.072\.0Decomposed\+Semantic\(Sage\)1387\.218\.176\.8Goedel\(Finetuned\)20456\.974\.519\.6The three reported categories are defined as follows\.Wrong Injection:SFS\_\{\\mathrm\{F\}\}hard\-codes a concrete answer absent from the openSNLS\_\{\\mathrm\{NL\}\}\.Mathematically False:the judge treatsSFS\_\{\\mathrm\{F\}\}as asserting a false claim\.Existential:a faithful open encoding is rejected primarily for omitting an explicit answer\.

The empirical split matches the prompt\-level bias above\. Monolithic generators and fine\-tunedGoedelare dominated by Mathematically False and Wrong Injection \(Goedel:74\.5%74\.5\\text\{\\,\}\\mathrm\{\\%\}and56\.9%56\.9\\text\{\\,\}\\mathrm\{\\%\}of rejects\): they guess a closed witness and often encode an incorrect constant\. Decomposed generators, includingSage, are dominated by Existential \(76\.8%76\.8\\text\{\\,\}\\mathrm\{\\%\}\): they keep open encodings \(∃x,P⁡\(x\)\\exists x,\\,P\(x\)\) that the judge systematically prefers less than explicit answers\. This asymmetry is intentional under our loop contract\. Our in\-loop rater is not trained or prompted to verify the mathematical correctness of conjectured constants; doing so would require solving the informal problem and would conflate translation with deduction\. We therefore treat both injection and existential texture as admissible, and we do not route pure mathematical\-falsity rejections—especially wrong injected witnesses—through the correction loop\. Accordingly, the residualGoedel\-SMgap should not be read as a failure of decomposition: forGoedeland monolithic methods it largely reflects unsuccessful guessing, whereas forSageit largely reflects the judge’s documented preference against open existential formalizations\.

## Appendix DComprehensive Performance Results and Trajectory Analysis

We expand the generator\-backbone scaling results of[Table3](https://arxiv.org/html/2609.35790#S6.T3)and the human validation ofSage\-SMsummarized in[Section6](https://arxiv.org/html/2609.35790#S6), reporting the full metric suite, witness\-injection rates, and the stratified audit design\.

### D\.1Generator Backbone Ablation: Scaling across Model Generations

To verify that the performance ofSageis not contingent upon the specific inductive biases of Qwen3\.6\-27B, we evaluated our complete decomposed semantic pipeline \(Sage,T=5T=5, pass@1\) across three successive model generations: Qwen3\-32B, Qwen3\.6\-27B, and Qwen3\.8\-27B\. All runs were conducted onOmni\-MATHin the Answer\-Aware setting and audited using identical protocols: Lean 4 type\-checking \(Compile\), unanimous 4/4 independent Gemma4\-31B consensus \(Goedel\-SM\), our multi\-dimensional semantic gate \(Sage\-SM\), and our witness injection audit\.

Table 12:Comprehensive generator backbone ablation onOmni\-MATH\(Answer\-Aware, pass@1,N=300N=300\)\.All methods useSagewith identical prompting, repair budgets \(T=5T=5\), and independent judge protocols\. Joint solved counts reported out of 300 problems\.Model BackboneCompileGoedel\-SMCompile∧\\wedgeGoedel\-SMJoint CountCompile∧\\wedgeSage\-SM∗WitnessInjection \(%\)Qwen3\-32B \(32B\)57\.346\.330\.391 / 30052\.322\.0Qwen3\.6\-27B \(27B\)96\.080\.377\.3232 / 30093\.790\.2Qwen3\.8\-27B \(27B\)98\.086\.385\.7257 / 30095\.789\.5##### Analysis of Scaling Trajectories\.

The empirical progression highlights two clear behaviors:

1. 1\.Monotonic Verification Synergy:As the generator’s underlying formal competence improves, the efficacy of the repair loop compounds dramatically\. While Qwen3\-32B struggles to interpret Lean 4 compiler diagnostics \(yielding only57\.3%57\.3\\text\{\\,\}\\mathrm\{\\%\}compilation and30\.3%30\.3\\text\{\\,\}\\mathrm\{\\%\}joint fidelity\), Qwen3\.8\-27B reaches98\.0%98\.0\\text\{\\,\}\\mathrm\{\\%\}compilation and85\.7%85\.7\\text\{\\,\}\\mathrm\{\\%\}joint fidelity\.
2. 2\.Witness Extraction Ceiling:In Answer\-Aware formalization, injecting the target constant from the informal proof is expected\. Qwen3\-32B achieves only22\.0%22\.0\\text\{\\,\}\\mathrm\{\\%\}witness injection, indicating frequent comprehension failures on informal mathematical texts\. In contrast, both Qwen3\.6\-27B \(90\.2%90\.2\\text\{\\,\}\\mathrm\{\\%\}\) and Qwen3\.8\-27B \(89\.5%89\.5\\text\{\\,\}\\mathrm\{\\%\}\) reach the witness extraction ceiling\. Consequently, the performance improvement between 3\.6 and 3\.8 is purely driven by superior formalization fidelity, syntax resolution, and premise alignment\.

## Appendix EHuman Expert Validation of the Semantic Gate

To evaluate the reliability of our automated quality gate, three Lean\-proficient annotators independently scored an adversarial audit corpus ofN=45N=45zero\-shotOmni\-MATHformalizations under the same five\-core rubric and binary gate used bySage\-SM\. We compare the automated gate tomajority vote\.

##### Stratified Audit Design\.

Rather than drawing a naive uniform random sample \(which would be dominated by straightforward instances\), the benchmark was deliberately stratified across four distinct categories to stress\-test the gate against edge cases:

1. 1\.Silent Semantic Failures \(N=25N=25\):Statements that compile cleanly in Lean 4 but contain subtle mathematical flaws \(e\.g\., incorrect summation indices, artificial domain restrictions, or hardcoded constants\)\.
2. 2\.Compile\-Failed Faithful Drafts \(N=10N=10\):Mathematically sound translations that failed type\-checking solely due to minor syntactic or import errors\.
3. 3\.Verified Clean Translations \(N=5N=5\):Idiomatic, fully compilable, and semantically equivalent formalizations\.
4. 4\.Catastrophic Failures \(N=5N=5\):Formalizations that are both uncompilable and mathematically false\.

##### Results\.

Across the stratified audit, the automated gate concurs with majority human judgment on71\.1%71\.1\\text\{\\,\}\\mathrm\{\\%\}of formalizations\. Beyond the binary decision, mean human Semantic Match aligns with the rater at Pearsonr=0\.64r=0\.64and Spearmanρ=0\.63\\rho=0\.63, providing complementary evidence that the evaluator ranks drafts consistently with human semantic preference\.