1 Introduction↩︎

Large language models (LLMs) have demonstrated strong mathematical problem-solving ability [1], while proof assistants such as Lean 4 [2] provide a trusted kernel for checking formal syntax, types, and proofs. Much of the recent Lean AI benchmark and systems literature therefore focuses on theorem proving: given a fixed formal statement, generate a proof that the checker accepts [3]–[7]. This setting has a clean success criterion. If the statement is fixed and trusted, checker acceptance of the proof is a strong evaluation signal.

Natural-language-to-Lean statement formalization has a different failure mode. Here the model generates the formal statement itself. Lean can verify that a declaration is well-typed, but it cannot verify that the declaration expresses the same mathematical meaning as the original natural-language theorem. A compiling statement may omit a hypothesis, change the domain, strengthen or weaken the claim, or encode a vacuous version of the result. Thus compilation is an essential validity filter, but not a sufficient measure of success. Prior work has recognized this problem through reference-pair benchmarks such as ProofNet [8], filtering pipelines using compilation, back-translation, NLI, or human checks [9], compiler/back-translation checks for Lean 4 translators [10], alignment evaluators [11], and faithful equivalence metrics such as BEq [12]. We take this distinction as the central evaluation problem.

This paper studies faithful statement formalization: translating natural-language mathematics into Lean 4 theorem declarations that both compile and preserve the intended meaning. We evaluate this task on a curated benchmark of 400 graduate-level statement entries drawn evenly from real analysis, complex analysis, topology, and algebra. Our evaluation combines compiler verification with semantic faithfulness scoring by independent LLM judges, strict consensus reporting, and human expert calibration. The resulting metric is not a formal equivalence proof; it is a calibrated semantic filter intended to support system comparison and to expose compile-valid but meaning-shifted statements at scale.

We compare general-purpose LLMs, dedicated statement formalizers (Herald Translator [10], Kimina-Autoformalizer [5], [13], and StepFun-Formalizer [14]), prover-oriented Lean models (Kimina-Prover and Goedel-Prover [5], [7]), and tool-augmented agents under the same validity-and-faithfulness metric. For the systems we test, Lean-specialized and proof-oriented training do not by themselves yield high faithful statement generation under a statement-only protocol.

The central empirical finding is that the semantic bottleneck remains visible even after strong validity repair. The full agent compiles most outputs, but nearly one third of benchmark entries land in the compile-pass but consensus-unfaithful bucket, and human review confirms that this bucket is usually a real semantic failure. This is a measurement study with three interlocking artifacts: a graduate-level benchmark, a human-calibrated faithfulness metric, and a factorial decomposition of common pipeline interventions.

We then use factorial ablation to attribute gains across three common intervention axes: parametric drafting, Mathlib/context grounding, and Lean elaboration feedback. The decomposition shows that elaboration feedback dominates validity repair, search mainly helps grounding and efficiency, and fine-tuned drafting is largely redundant in this tool stack once feedback and grounding are available. This shifts the contribution away from the familiar observation that verifier feedback is useful: the point is to measure which interventions improve formal validity, which improve semantic faithfulness, and which merely make the repair trajectory cheaper.

1.0.0.1 Contributions.

First, we assemble a graduate-level benchmark from open mathematical sources and pair it with a human-calibrated consensus LLM-as-Judge metric for statement formalization, combining Lean validity with GPT-5.2/Gemini semantic consensus. Human audits show high precision for consensus-positive labels and confirm that most audited consensus-negative compile-pass outputs are genuine semantic failures, making the metric a conservative operating point rather than an equivalence proof. Second, we use this protocol to quantify the compile-pass gap and to compare general-purpose LLMs, specialized formalizers, prover-oriented Lean models, and tool-augmented agents under one metric. Third, we use factorial design as bottleneck attribution, separating the effects of parametric drafting, Mathlib/context grounding, and Lean elaboration feedback on validity, faithfulness, and efficiency. We release the benchmark, agent implementation, evaluation scripts, and tool-call logs to support reproducible analysis of successful and failed formalization trajectories.

2 Problem Setting↩︎

We address the task of statement formalization: automatically translating natural-language mathematical statements into valid Lean 4 theorem declarations. This task is the first step before proof search: it bridges informal human intent and machine-checkable syntax, but it does not attempt to prove the resulting declaration.

2.0.0.1 Statement formalization vs.theorem proving.

The distinction matters for evaluation. In theorem proving benchmarks, the formal statement is fixed; the system succeeds when it produces a proof accepted by the checker. In statement formalization, the statement is generated. The checker can reject ill-typed code, but it cannot decide whether a type-correct declaration is the intended translation of the natural-language input. Our benchmark and metrics therefore evaluate generated declarations, not proof search against trusted declarations.

2.1 Task Definition↩︎

Formally, let \(\mathcal{X}\) be the space of informal mathematical statements and \(\mathcal{Y}\) be the space of valid Lean 4 declarations. Given an input \(x \in \mathcal{X}\), the system must generate a statement \(y \in \mathcal{Y}\) satisfying three criteria: syntactic validity (it compiles in Lean 4 with Mathlib), statement-centricity (it omits proofs via := by sorry), and semantic faithfulness (it expresses the same mathematical claim as \(x\)).

2.2 Evaluation Context↩︎

Most recent Lean benchmarks study proof search rather than statement generation. MiniF2F provides fixed formal Olympiad statements for cross-system theorem proving [3]; LeanDojo extracts formal theorems and proofs from Mathlib and evaluates models by whether they can complete proofs from proof states [4]; recent formal reasoning models such as DeepSeek-Prover, Kimina-Prover, and Goedel-Prover report progress largely through proof-generation success on supplied formal Lean statements [5]–[7]. In these settings, checker acceptance is a strong evaluation signal because the formal target statement is already specified.

Statement autoformalization has a different evaluation burden. ProofNet pairs natural-language undergraduate theorems with Lean 3 statements and evaluates statement translation against references [8]. Lean Workbook constructs a large Lean problem set from natural-language problems and filters generated statements using compilation, back-translation, NLI, and human examination [9]. Herald trains a dedicated statement translator and validates generated statements with Lean compiler and LLM back-translation checks [10]. StepFun-Formalizer trains dedicated autoformalization models and evaluates them with syntax checks and BEq-style equivalence to gold formal statements [12], [14]. PDA studies process-driven Lean 4 autoformalization over statements and proofs and uses compiler-derived process feedback to train a verifier [15]. FormalAlign evaluates informal–formal semantic alignment directly [11]. Most directly for statement-level equivalence, Liu et al. [12] propose BEq, a neuro-symbolic equivalence metric evaluated against expert-annotated formal-statement equivalence labels.

Our setting is complementary to reference-based equivalence metrics such as BEq [12]: our benchmark consists of natural-language textbook statements without gold Lean declarations. Rather than replacing formal equivalence checking, we use compiler validity, cross-model semantic judging, and human expert calibration as an operational metric for system comparison, then study what this metric reveals about model families and tool categories.

2.3 Dataset Construction↩︎

To benchmark this task, we curated a dataset of 400 graduate-level statement entries derived from open-source LaTeX lecture notes and textbooks. We selected sources that provide natural-language statements without accompanying formal code, ensuring the task represents genuine translation rather than retrieval. As detailed in Table 1, the dataset is balanced across four domains—Real Analysis, Complex Analysis, Topology, and Algebra—with 100 examples from each; all benchmark rates are reported per entry rather than as counts of unique theorem schemas.

2.4 Evaluation Protocol↩︎

To evaluate generated statements, we adopt a two-stage Consensus LLM-as-Judge protocol. First, we apply a Compiler Verification filter: any code that fails to compile is not faithful. Second, for compiling code, two independent LLM judges—GPT-5.2 in Medium Thinking mode and Gemini-2.5-Pro—compare the generated Lean declaration against the original natural-language input and assign statement-level faithfulness scores on a 0–10 scale. The judge prompt and rubric (Appendix 10) were reviewed and adjusted by a Lean 4–experienced researcher to align the evaluation with statement-level meaning. Human calibration of this automated metric is reported in Section 4.1.

The metric is not intended to certify mathematical truth or proof completeness; it is intended to detect whether a compiling declaration preserves the intended statement.

We therefore treat the strict consensus threshold as a high-precision operating point for comparison, and separately audit negative buckets to measure how conservative it is.

Success Metric: We define a generated translation \(y\) for an input statement \(x\) as Faithful if and only if it compiles and both semantic judges score it at least 9: \[\text{Compiles}(y)=\text{True} \quad \boldsymbol{AND} \quad \min\{\text{Score}_{\text{GPT}}(x,y),\text{Score}_{\text{Gemini}}(x,y)\}\ge 9 ,\] where the two score functions are implemented by GPT-5.2 and Gemini-2.5-Pro, respectively.

2.4.0.1 Cross-judge consensus.

Across systems, Gemini-2.5-Pro consistently accepts more outputs than GPT-5.2, and most GPT-5.2 positives are also accepted by Gemini. Because our reported consensus label requires both judges, it is best viewed as an intersection rule accompanied by an empirical high-overlap pattern: \[\mathrm{Pass}_{\text{Consensus}} =\mathrm{Pass}_{\text{GPT}}\cap \mathrm{Pass}_{\text{Gemini}}, \qquad \frac{|\mathrm{Pass}_{\text{GPT}}\cap \mathrm{Pass}_{\text{Gemini}}|}{|\mathrm{Pass}_{\text{GPT}}|} \;\text{is high empirically}.\] Table 2 summarizes this GPT-to-Gemini empirical coverage at the system-family level; Appendix Table 8 gives the full per-system counts and the small number of GPT-only exceptions, and Appendix Figure 3 shows domain-level judge disagreement. Because the rows aggregate different numbers of systems, the consensus/GPT ratio rather than the raw count is the relevant quantity. This pattern supports using strict GPT\(\cap\)Gemini consensus as a conservative reported faithfulness metric.

4.5pt

3 Formalization Pipeline and Tool Factors↩︎

The agent architecture, illustrated in Figure 1, is structured as a controlled implementation of three common remedies in autoformalization pipelines: drafting from a Lean-specialized prior, grounding through search, and repairing through verifier feedback. The core component is a central LLM orchestrator (GPT-5.2) that interacts with the Lean 4 environment via a defined API. Unlike static prompting, this architecture allows the model to maintain a persistent state, observing compiler errors, retrieved symbols, or draft translations before deciding on the next step. This design decouples natural-language reasoning from formal checking: Lean supplies high-precision validity feedback, while the orchestrator remains responsible for preserving the mathematical meaning of the input statement.

The purpose of this architecture is diagnostic rather than architectural novelty: it exposes separable information channels so that the same benchmark can ask which channel moves validity, faithfulness, or efficiency.

3.1 Tools and the Bottlenecks They Target↩︎

We equip the agent with tools that target different bottlenecks in statement formalization. Expert Drafting (T) is a parametric translation prior: the lean4_translator tool requests a specialized Lean statement draft from the fine-tuned Herald model before the general orchestrator edits or verifies it. Knowledge Search (S) provides Mathlib/context grounding through symbol lookup tools such as lean_inspect_name and lean_resolve_name, together with general web search; these tools return identifier candidates, types, and definitions, but they are not a dedicated semantic retrieval system such as LeanSearch [20]. Compiler Feedback (F) exposes Lean elaboration feedback through the lean_repl_runner, giving whole-statement validity checks and error messages for syntax, type, namespace, and elaboration repair.

We treat drafting (T), search (S), and elaboration feedback (F) as the three binary factors of a \(2^3\) factorial study; the full design and notation are deferred to Section 5. Detailed specifications of the tool definitions and signatures are provided in Appendix 9.

3.2 Controlled Prompt Assembly↩︎

To avoid confounding tool effects with prompt wording, all configurations use the same role definition and Lean-generation instructions: the agent must translate rather than prove, produce one theorem declaration ending in := by sorry, import Mathlib, and avoid invented definitions or axioms. The only part that changes is the tool-availability block, which declares which tools the agent may call. Thus, the factorial analysis varies access to drafting, search, and feedback tools while holding the task definition, output requirements, and anti-hallucination instructions fixed. Full prompt templates are provided in Appendix 9.

4 Performance Evaluation↩︎

4.1 Human Expert Validation↩︎

Before comparing systems, we summarize the human audit only to establish that the consensus metric is usable. Lean 4 reviewers re-scored targeted audit samples with the same 0–10 rubric. Applying each audit’s case-level decision rule first, then pooling the positive-bucket audits, gives 194/202 = 96.0% human-confirmed precision: 130/133 from the custom-agent strict-consensus subset and 64/69 from the independent three-reviewer Batch-B audit. For compile-pass consensus-negative outputs, the corresponding pooled confirmation rate is 112/136 = 82.4%: 95/114 from the custom-agent negative bucket and 17/22 from Batch B. Thus strict consensus is a high-precision, conservative operating point rather than an equivalence proof; Appendix 12 gives the full table, protocol, reviewer coverage, strictness analysis, and case studies.

4.2 Main Results↩︎

Figure 2 presents performance on the 400-entry benchmark across general LLMs, specialized formalizers, prover-oriented Lean models, and the full tool-augmented agent. One-shot systems without tools remain far below the full agent: the general-purpose LLM baselines shown here reach 19.8–28.0% consensus faithfulness, specialized formalizers reach 9.0–12.3%, and prover-oriented models reach only 4.0–5.0%. Compilation alone would substantially overstate progress: for example, Goedel-Prover compiles 19.2% of statements but is consensus-faithful on only 5.0%. In contrast, the full tool-augmented agent framework (\(T_{\max}=24\)) boosts compilation to 89.5% and consensus faithfulness to 60.5%.

In prover-oriented runs, despite an explicit statement-only prompt requiring declarations ending in := by sorry, models frequently emit proof-oriented reasoning, tactic bodies, malformed declarations, or no extractable Lean statement. We therefore treat these baselines as a transfer diagnostic from proof training to statement generation, not as proof benchmarks. The conservative conclusion is not that prover models lack formalization ability in general, but that proof-oriented Lean competence does not automatically transfer to prompt-following, statement-centric, semantically faithful formalization when the formal target statement is not supplied.

The metric also changes the interpretation of tool-agent performance. The full agent’s 89.5% compile rate might suggest that the task is close to solved under compiler-only evaluation. Under semantic consensus, however, 116/400 entries compile but are not accepted as faithful, a 29.0-point compile-pass/faithfulness gap visualized in Figure 2; the Batch-A human audit confirms most reviewed cases in this bucket as genuine semantic mismatches. This compile-pass gap is the main empirical gap studied in the remainder of the paper.

Aggregate scores also hide substantial per-instance complementarity across tool settings (Table 3). The all-tools configuration is strong but not uniformly dominant: some cases it misses are solved by leaner configurations, and most of these recoverable misses already compile under 111 but fail strict semantic consensus. This makes the remaining bottleneck sharper than “REPL helps”: tool access changes the formalization trajectory, and the open problem includes per-instance routing or early stopping. Trajectory length is a useful warning signal specifically when feedback is enabled: pooling the four \(F{=}1\) configurations, faithfulness falls from 81.3% for 1–2 step runs to 12.0% for 19–24 step runs; across the nonempty no-feedback configurations, the corresponding drop is only 32.0% to 17.0% (Appendix Table 20).

8pt

Additional orchestrator checks with Sonnet 4.5 and Gemini-2.5-Pro show the same pattern: all three 111 agents reach 60–65% consensus faithfulness despite different one-shot baselines (Figure [fig:multi95model]; full table in Appendix 14.5).

5 Bottleneck Decomposition↩︎

Aggregate accuracy collapses three different questions: whether an output compiles, whether it preserves the intended statement, and how much tool interaction it costs. A tool can raise compile rate while enlarging the compile-pass but semantically rejected bucket, so the diagnostic target is not just which tool helps on average, but which boundary each tool moves: validity, faithfulness, or efficiency.

5.1 Factorial Design over (T,F,S)↩︎

Formally, each tool setting is a bit vector \[c=(t,f,s)\in\{0,1\}^3,\qquad \mathcal{C}=\{000,001,010,011,100,101,110,111\},\] where the bits denote access to (T,F,S). We run every benchmark item under every \(c\in\mathcal{C}\) and evaluate metrics \(m(c)\) such as compile rate, consensus-faithful rate, and tool cost. Main effects are high-minus-low averages over the other factors; for example, \[\Delta_F(m)=\frac{1}{4}\sum_{t,s\in\{0,1\}}\bigl[m(t,1,s)-m(t,0,s)\bigr].\] Thus 111 is the full tool-augmented agent, while 000 is the One-Shot Baseline established in Section 4. The remaining seven configurations selectively toggle tool definitions in the system prompt while holding the task prompt fixed.

5.2 Main Effects: Validity vs. Faithfulness↩︎

Table 4 reports performance across all configurations, with each row comparing the same \((T,S)\) setting before and after elaboration feedback (F). To quantify the contribution of each factor, we compute standard factorial main and interaction effects, defined as differences in mean response between the high and low levels of a factor (averaged over the other factors).

5pt

Beyond final accuracy, the key pattern is that tools move different boundaries. Feedback greatly expands validity: \((000)\to(010)\) increases compiled outputs from 105 to 366 and faithful outputs from 79 to 245, but also increases the compile-pass semantic gap from 26 to 121. Search has a different role: when feedback is enabled, it slightly changes final faithfulness but improves semantic selectivity, reducing the compile-pass gap from 121 to 101 for \(T=0\) and from 139 to 116 for \(T=1\). The full conditional table and tool-usage counts are in Appendix 13.

7pt

5pt

Feedback is therefore the largest validity intervention, but it is not a semantic oracle: it moves many noncompiling cases into both the faithful and compile-pass-but-unfaithful buckets. The domain split in Table 6 shows why this matters. Complex Analysis converts most feedback-driven validity gains into faithful statements, while Algebra and Topology gain far less in final faithfulness; for Topology, this pattern is consistent with advanced Mathlib encoding and coverage constraints in examples involving covering spaces and fundamental groups. Search improves final faithfulness mainly without feedback (\(\Delta_S(F{=}0)=+12.4\) pts vs. \(\Delta_S(F{=}1)=+1.2\) pts), and with feedback it mainly improves selectivity and efficiency: REPL calls fall by 29.8% for \((010)\to(011)\) and 26.6% for \((110)\to(111)\). The translation prior is not the limiting bottleneck in this tool stack: it helps without feedback (\(\Delta_T(F{=}0)=+3.9\) pts) but slightly hurts with feedback (\(\Delta_T(F{=}1)=-2.0\) pts), suggesting substitutability once a strong orchestrator has compiler feedback and grounding.

5.3 Interactions and Per-Item Trajectory Churn↩︎

The negative interactions make the result more specific than “REPL helps.” Search and feedback partially substitute because both expose Mathlib-grounded information: search gives targeted symbol/type information, while feedback gives whole-statement elaboration diagnostics. Under this setup, Search is most valuable as a capability tool when feedback is absent and as an efficiency/selectivity tool when feedback is present. The same regime dependence appears for the translation prior: a specialist draft is useful in low-tool settings, but can anchor the repair loop once feedback is available. We treat this as an empirical observation about this tool stack, not as a claim that fine-tuned Lean translators are generally unnecessary.

The per-item transitions behind these aggregate effects are strongly nonmonotone (Table 7). Thus small net interaction effects can hide large trajectory churn. The useful design question is therefore not only which tool improves the average rate, but when an orchestrator should trust, ignore, or stop after a tool-induced repair path. This motivates per-instance routing or early-stopping policies, and the released trajectory logs are intended to support that follow-on analysis: final scores alone do not distinguish a clean first translation from a long repair loop that eventually compiles the wrong statement.

6pt

6 Limitations↩︎

Our task is translating natural language into valid Lean 4 statement declarations, not generating proofs. Provability is a useful downstream sanity check, but it is neither necessary nor sufficient for statement faithfulness: a faithful declaration may be hard to prove automatically, while a provable declaration may formalize the wrong claim. Similarly, our LLM-as-judge metric is a scalable semantic audit, not a formal equivalence proof. Human audits support high positive precision and confirm that most rejected compile-pass outputs are real semantic failures, but 24/136 (17.6%) audited compile-pass negative-bucket cases are human-rescued faithful cases, so strict consensus should be interpreted as conservative. The main orchestrator and one judge are from the same model family; the Sonnet/Gemini orchestrator checks and the human audits mitigate, but do not eliminate, this possible dependence.

The benchmark covers 400 statements from four open mathematical sources across four graduate areas; broader textbook coverage and research-level statements remain out of scope. The Search factor measures the retrieval tools implemented in this agent—Mathlib symbol lookup, namespace resolution, and general web search—not a dedicated semantic retriever such as LeanSearch [20]. Stronger retrieval may change the Search main effect and the \(F{\times}S\) interaction. Finally, tool-augmented formalization is more expensive than one-shot generation; although Search reduces compiled iterations, the full REPL loop remains a barrier to real-time interactive use.

7 Conclusion↩︎

Statement formalization should be evaluated as meaning preservation, not only as Lean acceptance. The central lesson is that execution feedback can make many more declarations type-check, but it does not decide whether the checked object is the intended theorem. Human-calibrated semantic evaluation makes this gap visible and gives a conservative way to compare systems at scale.

The bottleneck analysis also shows that tools are not monotone add-ons. Feedback, search, and drafting can help, interfere, or change failure modes depending on domain and trajectory, so average gains alone are not enough to understand a formalization pipeline. This suggests a more diagnostic view of autoformalization: the system should know when it is repairing syntax, when it is searching for the right mathematical interface, and when continued repair is likely to drift away from the original statement. Future systems should therefore pair strong Lean feedback with semantic evaluation and policies that decide when to search, repair, restart, or stop.

8 Artifact Availability↩︎

An anonymized repository containing the agent code, benchmark files, generated results, evaluation scripts, tool-call logs, and human-check materials is available at https://anonymous.4open.science/r/neurips_happy_submission_anon-4AFF/README.md.

9 Agent Implementation Details↩︎

9.1 Prompt Assembly↩︎

The system prompt is constructed from three modular components: (i) a task definition establishing the core translation objective, (ii) a general usage guide containing fixed best practices for Lean 4 code generation, and (iii) a capability block that is dynamically populated based on the factorial configuration \((T,F,S)\). This structure holds the agent’s semantic goal and coding standards (i and ii) fixed, while selectively enabling or disabling external tools (iii) to isolate the causal effect of each capability. We assemble (i) and (ii) into a Shared Base Prompt, shown below, while the capability block definitions are provided in Appendix 9.3.

9.2 Shared Base Prompt↩︎

9.3 Tool-Availability Blocks↩︎

Each factorial configuration \((T,F,S)\) determines which tools are exposed to the agent. We implement this by a modular prompt template in which the AVAILABLE TOOLS block is constructed by including the corresponding tool-specification entries and omitting inactive ones. We show the complete tool block for the fully enabled configuration \((1,1,1)\) below; other configurations are obtained by deleting the entries for tools that are disabled.

9.4 Tool Interfaces↩︎

9.5 Example Execution Trace↩︎

10 LLM-as-a-Judge Prompt and Rubric↩︎

We evaluate semantic faithfulness using an LLM-as-a-judge that receives: (i) the natural-language statement, (ii) the generated Lean 4 code, and (iii) a boolean compile_pass. The judge outputs a JSON object with fields faithful and grade (0–10). If compile_pass=false, we require faithful=false and restrict the grade to 0–3. The translation is considered as faithful if and only if the code compiles and the score is \(>=9\).

You are an expert in Lean 4, Mathlib, and mathematics. You are judging TRANSLATION-ONLY.

Input: (1) a natural-language statement, (2) a Lean 4 code snippet, (3) compile_pass boolean.
Your job: decide whether the Lean code, AS A STATEMENT, matches the meaning of the natural-language statement.

Key policy (NOT PICKY):
- If compile_pass = False: the translation is NOT faithful. grade must be 0..3. faithful=false.
- If compile_pass = True: ignore the proof/body entirely (including `by sorry`). Proof completeness is NOT part of the evaluation.
- A translation is faithful if the Lean statement expresses the same mathematical claim as the NL statement.

Auxiliary definitions policy (lenient but not allowing cheating):
- Auxiliary defs/lemmas are allowed if they are reasonable encodings/abbreviations and do not change the meaning.
- However, if the code introduces a clearly vacuous placeholder for a nontrivial concept (e.g. `def X := True`, `:= none`, `:= 0` for something meant to be meaningful), and that placeholder is essential to making the final theorem appear to match, then the translation is NOT faithful.

How to judge meaning (focus):
- Compare the MAIN theorem/definition statement(s) to the NL statement.
- Check quantifiers (forall/exists), logical structure (->/<->/and/or), and key hypotheses.
- Check main objects/domains: Nat/Int/Real, rings/groups, ZMod n, matrices, etc.
- Small implementation details are OK if the meaning is preserved.

Scoring guide (integer 0..10):
- 0: unrelated.
- 1-3: compile_pass is False OR statement is clearly wrong.
- 4-6: compiles, but meaning is materially different / missing key hypotheses / wrong domain;
       might be "in the ballpark".

- 7-8: compiles, mostly matches, but has a noticeable mismatch (e.g. strengthened/weakened in an important way).
- 9: compiles, very close; only tiny mismatch.
- 10: compiles and meaning matches.

Output contract (STRICT):
Return a single JSON object with exactly these fields:
{
  "faithful": true or false,
  "grade": 0..10,
  "thought": "### BEGIN THOUGHT\n<short explanation focusing on statement-level comparison>\n### END THOUGHT"
}
Return ONLY valid JSON. No extra keys. No markdown outside JSON.

11 Additional Metric Validation Results↩︎

4.5pt

Across all rows in Table 8, the GPT-only column sums to 39 out of 2176 GPT-positive labels (1.8%). Thus GPT positives are almost always, but not literally always, accepted by Gemini.

Figure 3 shows that the remaining disagreements are not uniformly distributed across domains. Real Analysis accounts for the largest number of conflicts (125), followed by Algebra (82), Complex Analysis (61), and Topology (58). This aligns with the domain difficulty results: under the full agent setting (config=111), Real Analysis has the lowest Faithful rate among the four domains (Table 21), leaving more borderline cases for judges to interpret.

12 Human-Check Validation Details↩︎

This appendix reports the human-review protocol behind Table 9. We keep the audit identities separate: Reviewer 1 audits consensus-positive outputs from the custom agent, Batch A audits the custom agent’s compile-pass but consensus-unfaithful bucket, and Batch B evaluates a separate 100-case Aristotle system run. Rates are computed within each blinded audit batch on the same case_id; cross-audit theorem-name overlap is diagnostic only and is not pooled as if it were the same Lean output.

12.0.0.1 What kind of “soundness” is supported?

The audits support an operational soundness claim for the reported metric: if an output is counted as faithful by strict GPT\(\cap\)Gemini consensus, human reviewers usually agree that it preserves the statement meaning; if a compile-passing output is rejected by strict consensus, it is usually a real semantic mismatch rather than mere evaluator noise. This is not a formal proof of semantic equivalence, and it is not a recall guarantee. In particular, the compile-pass negative-bucket audits show that strict consensus is conservative: 24/136 (17.6%) audited cases are rescued by human majority. The appropriate interpretation is therefore: strict consensus is a high-precision, conservative decision boundary for large-scale system comparison, with human-audited evidence on both sides of the boundary.

6pt

4pt

12.0.0.2 Reviewer score threshold and majority rule.

Human reviewers used the same 0–10 semantic faithfulness scale as the LLM judges. A score \(\geq 9\) is treated as faithful. Majority labels require at least two numeric human scores on the same blinded case_id; compile failures are counted as unfaithful even if a reviewer notes that the intended mathematical content looks close. This compile-aware rule matches the paper metric, where faithfulness requires both compilation and semantic agreement. In the three-reviewer Batch A/B audits, reviewers also self-reported their use of LLM assistance: Reviewer 2 reported no LLM assistance, while Reviewers 3 and 4 each reported low assistance (2/10 on a 1–10 usage scale). Reviewer 1 did not provide a self-report for this field.

4.5pt

The individual-reviewer table is useful because it shows that the calibration result is not produced by one unusually permissive reviewer. Reviewers differ substantially: Reviewer 2 is more likely to rescue Batch-A LLM-negative cases, while Reviewer 4 is stricter and more aligned with the LLM boundary. The majority rule averages over these differences and is the reported estimator for the three-reviewer audits.

5pt

Batch A shows that the custom-agent negative bucket is not merely judge over-conservatism: among 114 cases with sufficient same-case human coverage, human majority confirms 95 as unfaithful (83.3%) and rescues 19 as faithful (16.7%). Because all Batch-A items compile, this directly supports the compile-pass but semantically unfaithful gap highlighted in Figure 2.

4.5pt

Table 13 gives the most direct same-case calibration view. In Batch B, the automatic and human-majority labels agree on 87/97 effective cases (89.7%). The off-diagonal cells are balanced: five consensus positives are rejected by human majority, and five consensus negatives are rescued by human majority. Thus the Batch-B full-evaluation sample does not indicate a systematic inflation of the automatic faithful rate; its headline strict-consensus faithful rate is 70/98, while the human-majority faithful rate is 69/97.

5pt

5pt

The harsh variants are not used as the headline metric because they conflate semantic correctness with reviewer coverage and strict unanimity. They are useful as stress tests: even under unanimous-reviewer requirements, many consensus-positive outputs remain faithful, while the majority metric is the appropriate operating point for comparing systems at scale.

4.5pt

The intervals reinforce the qualitative conclusion without overclaiming. Positive precision is high in both the original custom-agent audit and the independent Batch-B audit. Compile-pass negative-bucket confirmation is also high, but its interval is wider in Batch B because there are only 22 compile-pass consensus-negative cases with majority coverage. The false-negative rates are not negligible: Batch A rescues 19/114 consensus-negative cases, and Batch B rescues 5/22 compile-pass consensus-negative cases. This is why the main paper describes strict consensus as conservative rather than complete.

12.1 Compact Human-Check Case Studies↩︎

The following audited examples give the original natural-language statement, the translated Lean 4 code, GPT/Gemini judge scores, and all available anonymized human-reviewer scores. The first five show boundary or off-diagonal cases; the next five are strict-consensus positives from Batch B where all three same-case reviewers scored the output faithful. Human scores use the 0–10 rubric, with scores \(\geq 9\) treated as faithful; R1–R4 denote Reviewers 1–4, and “–” means that reviewer did not score that generated Lean output. When an R1 score is shown for a Batch B case, it is a theorem-name-overlap diagnostic rather than a same-output score; the same-output Batch B scores are R2–R4.

import Mathlib

open Set
open scoped Topology

theorem benmckay_top_covering_spaces_502
    (Z : Set ℂ) (hZ₁ : IsOpen Z) (hZ₂ : IsConnected Z)
    (g : ℂ → ℂ) (hg : AnalyticOn ℂ g Z) :
    (∃ G : ℂ → ℂ, AnalyticOn ℂ G Z ∧ ∀ z ∈ Z, g z = Complex.exp (G z)) ↔
      ((∀ z ∈ Z, g z ≠ 0) ∧
        ∀ x : ↥Z,
          ∀ γ : Path x x,
            ∃ γ0 : Path (g (x : ℂ)) (g (x : ℂ)),
              Path.Homotopic γ0 (Path.refl _))
  := by
  sorry

import Mathlib

theorem taylor_second_order_uniform_on_compact
    {n : ℕ} {f : (Fin n → ℝ) → ℝ} {U : Set (Fin n → ℝ)}
    (hconv : Convex ℝ U)
    (hC2 : ContDiffOn ℝ 2 f U)
    (hcont : ContinuousOn (fun x => fderiv ℝ (fun y => fderiv ℝ f y) x) U) :
    ∀ ⦃K : Set (Fin n → ℝ)⦄, IsCompact K → K ⊆ U →
      TendstoUniformlyOn
        (fun x : (Fin n → ℝ) =>
          fun y : (Fin n → ℝ) =>
            (f y - f x - (fderiv ℝ f x) (y - x) -
                (1 / (2 : ℝ)) *
                  (fderiv ℝ (fun z => fderiv ℝ f z) x) (y - x) (y - x)) /
              ‖y - x‖ ^ (2 : ℕ))
        (fun _ => (0 : ℝ))
        (⊥ : Filter (Fin n → ℝ))
        K := by
  sorry

import Mathlib

theorem contractible_connected_and_trivial_homotopyGroups
    (X : Type*) [TopologicalSpace X] [ContractibleSpace X] :
    ConnectedSpace X ∧ ∀ (n : ℕ) (x : X), Subsingleton (HomotopyGroup (Fin n) X x) := by
  sorry

import Mathlib

open CategoryTheory FundamentalGroupoid FundamentalGroupoidFunctor

noncomputable def «benmckay_top_fundamental-groups_336»
    (X : Type*) (Y : Type*) [TopologicalSpace X] [TopologicalSpace Y]
    (x₀ : X) (y₀ : Y) :
    FundamentalGroup (X × Y) (x₀, y₀) ≃* FundamentalGroup X x₀ × FundamentalGroup Y y₀ where
  toFun p := (Path.Homotopic.projLeft p, Path.Homotopic.projRight p)
  invFun q := Path.Homotopic.prod q.1 q.2
  left_inv p := Path.Homotopic.prod_projLeft_projRight p
  right_inv q := by
    ext
    · exact Path.Homotopic.projLeft_prod q.1 q.2
    · exact Path.Homotopic.projRight_prod q.1 q.2
  map_mul' a b := by
    set A := TopCat.of X
    set B := TopCat.of Y
    set pL := projLeft A B
    set pR := projRight A B
    show (pL.map (b ≫ a), pR.map (b ≫ a)) =
      (pL.map b ≫ pL.map a, pR.map b ≫ pR.map a)
    rw [pL.map_comp, pR.map_comp]

import Mathlib

theorem srdoty_alg_products_372
    (G H : Type*) [Group G] [Group H] :
    Function.Injective (MonoidHom.inl G H) := by sorry

import Mathlib

theorem jirilebl_ca_ca_19223 (z : ℂ) :
    ‖Complex.sin z‖ ≥ |Real.sin z.re| := by sorry

import Mathlib

theorem «jirilebl_ra_ch-several-vars-ders_3076»
    {n : ℕ} {U : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → ℝ}
    (_hU : IsOpen U) (_hf : DifferentiableOn ℝ f U) (hconv : ConvexOn ℝ U f)
    {x y : EuclideanSpace ℝ (Fin n)} (hx : x ∈ U) (hy : y ∈ U)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    f (t • x + (1 - t) • y) ≤ t * f x + (1 - t) * f y := by sorry

import Mathlib

theorem srdoty_alg_Z_n_513 {R : Type*} [Ring R] (a : R) : (-1) * a = -a := by sorry

import Mathlib

theorem benmckay_top_topology_551
    {X : Type*} [TopologicalSpace X] (A B : Set X) :
    closure (A ∪ B) = closure A ∪ closure B := by sorry

import Mathlib

open Filter Topology

theorem «jirilebl_ra_ch-seq-ser_1015» (x : ℕ → ℝ) (L : ℝ)
    (hx : Tendsto x atTop (nhds L)) :
    ∃ M : ℝ, M ≥ 0 ∧ Tendsto (fun n => max (x n) 0) atTop (nhds M) := by sorry

12.2 Four-Reviewer Theorem-Name Overlap Diagnostic↩︎

The Reviewer 1 audit and the three-reviewer audits were not designed as a four-reviewer repeated-measures study. Nevertheless, some theorem names occur in both the Reviewer 1 audit and the Reviewer 2/3/4 reviewed batches. Table 17 lists the cases where Reviewer 1 and all three later reviewers provided numeric scores. There are 32 such theorem-name overlaps: 3 in Batch A and 29 in Batch B. Exact Lean-code overlap with the Reviewer 1 audit is 0/32, so the table should be read as a diagnostic of reviewer strictness and theorem-level consistency, not as four humans scoring the same generated Lean declaration.

2.5pt

This overlap diagnostic is consistent with the main calibration story but is deliberately not used as the primary estimator. Among the 32 theorem-name overlaps, 29/32 have a four-reviewer majority faithful label and 25/32 are unanimous faithful. However, because exact Lean-code overlap with the Reviewer 1 audit is 0/32, these rows cannot be used to replace the within-batch same-case estimates in Tables 12–13. Their value is narrower: they show that when the same theorem names reappear in a later three-reviewer audit, the Reviewer 1 positive impression is usually not contradicted by the other reviewers, while the few disagreements identify cases where the theorem admits different generated formalizations or stricter reviewer interpretations.

13 Additional Factorial and Tool-Usage Details↩︎

5pt

5pt

7pt

14 Additional Domain Results↩︎

14.1 Domain Metrics under Full Configuration↩︎

14.2 Judge Scores by Domain↩︎

14.3 Domain-Level Feedback Effects↩︎

14.4 Domain-Level Effects of Search (S)↩︎

14.5 Multi-Model Orchestrator Comparison↩︎

To assess whether the framework’s gains are specific to the GPT-5.2 orchestrator or reflect structural properties of tool-augmented formalization, we evaluate two additional orchestrator models—Claude Sonnet 4.5 and Gemini-2.5-Pro—on the full 400-entry benchmark under the 111 (all tools) configuration.

7pt

As shown in Figure [fig:multi95model] and Table 25, all three models show large uplift from the tool-augmented framework (+148 to +163 faithful translations) and converge to 60–65% consensus-faithful outputs despite markedly different one-shot baselines (19–28%). This convergence suggests that the benefits of iterative tool use under the faithfulness metric are not specific to the GPT-5.2 orchestrator.

References↩︎