Paper deep dive
Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
Ke Zhang, Patricio Gallardo, Maziar Raissi, Sudhir Murthy
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 97%
Last extracted: 4/27/2026, 12:22:27 AM
Summary
This paper presents a systematic factorial analysis of tool-augmented LLM agents designed for formalizing natural language mathematics into Lean 4 code. The researchers investigate three tool categories: Fine-tuned Model Querying (Expert Drafting), Knowledge Search (Symbol Retrieval), and Compiler Feedback (Lean REPL). Using a benchmark of 400 graduate-level theorems across four mathematical domains, the study demonstrates that while all tools contribute, Compiler Feedback is the critical 'capability bottleneck' that enables high-success regimes, whereas Knowledge Search acts as a stabilizer and Expert Drafting is largely redundant when other tools are present.
Entities (11)
Relation Signals (4)
GPT-5.2 â actsasorchestratorfor â Compiler Feedback
confidence 100% ¡ The core component is a central LLM orchestrator (GPT 5.2) that interacts with the Lean 4 environment via a defined API.
Compiler Feedback â improves â Faithfulness
confidence 100% ¡ Enabling the REPL transforms the agent from a low-success regime into a high-success regime.
Herald â provides â Expert Drafting
confidence 100% ¡ the lean4translator tool requests a translation from the fine-tuned model Herald
Knowledge Search â stabilizes â Performance
confidence 90% ¡ Search is a stabilizer (+6.8pts)
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Automatic translation of natural language mathematics into faithful Lean 4 code is hindered by the fundamental dissonance between informal set-theoretic intuition and strict formal type theory. This gap often causes LLMs to hallucinate non-existent library definitions, resulting in code that fails to compile or lacks semantic fidelity. In this work, we investigate the effectiveness of tool-augmented agents for this task through a systematic factorial analysis of three distinct tool categories: Fine-tuned Model Querying (accessing expert drafts), Knowledge Search (retrieving symbol definitions), and Compiler Feedback (verifying code via a Lean REPL). We first benchmark the agent against one-shot baselines, demonstrating large gains in both compilation success and semantic equivalence. We then use the factorial decomposition to quantify the impact of each category, isolating the marginal contribution of each tool type to overall performance.
Tags
Links
- Source: https://arxiv.org/abs/2604.16538v1
- Canonical: https://arxiv.org/abs/2604.16538v1
Trouble viewing inline? Open PDF directly â
Full Text
45,643 characters extracted from source content.
Expand or collapse full text
Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis Ke Zhang 1 Patricio Gallardo 1 Maziar Raissi 1 Sudhir Murthy 1 Abstract Automatic translation of natural language math- ematics into faithful Lean 4 code is hindered by the fundamental dissonance between informal set- theoretic intuition and strict formal type theory. This gap often causes LLMs to hallucinate non- existent library definitions, resulting in code that fails to compile or lacks semantic fidelity. In this work, we investigate the effectiveness of tool- augmented agents for this task through a system- atic factorial analysis of three distinct tool cate- gories: Fine-tuned Model Querying (accessing expert drafts), Knowledge Search (retrieving sym- bol definitions), and Compiler Feedback (verify- ing code via a Lean REPL). We first benchmark the agent against one-shot baselines, demonstrat- ing large gains in both compilation success and semantic equivalence. We then use the factorial decomposition to quantify the impact of each cat- egory, isolating the marginal contribution of each tool type to overall performance. 1. Introduction Large language models (LLMs) have demonstrated remark- able capability in producing complex mathematical argu- ments (Castelvecchi, 2025), yet their probabilistic nature fundamentally conflicts with the absolute certainty required by formal mathematics. Proof assistants such as Lean 4 (de Moura & Ullrich, 2021) resolve this conflict by me- chanically verifying logical correctness, but they introduce a significant barrier: the âformalization bottleneck.â Most modern undergraduate and graduate-level theorems exist only in natural language and have not yet been translated into the strict syntax required by proof assistants (Lean Prover Community). Current attempts to automate translation into Lean 4 rely primarily on one-shot prompting or fine-tuning on static 1 University of California, Riverside. Correspondence to: Maziar Raissi <maziar.raissi@ucr.edu>. Preprint. April 21, 2026. datasets (Gao et al., 2025; Wang et al., 2025). Although these methods can generate plausible code, they face sev- eral fundamental obstacles. Training data for graduate-level mathematics is sparse, causing models to hallucinate nonex- istent theorems and symbols. Even when the mathematics is correct, a deep mismatch remains between the set-theoretic language of textbooks and Leanâs dependent type theory, making direct translation unreliable. Moreover, syntactic validity does not ensure semantic fidelity: Lean code may compile yet express a vacuous or incorrect statement. These issues are further compounded by the fact that Mathlib 4 is a fast-evolving, community-maintained library, so models trained on static snapshots frequently generate code that targets deprecated or nonexistent definitions in the current environment. To address these limitations, we introduce an agentic frame- work that replaces static generation with iterative refinement. A generalist LLM orchestrator interacts with three tool cate- goriesâsymbol retrieval, expert drafting, and Lean REPL feedbackâforming a closed loop of draft, verify, and re- pair that corrects both syntactic and semantic errors. Rather than treating this toolset as a black box, we apply a full factorial design on a new benchmark of 400 graduate-level theorems to quantify the causal contribution and interaction of each component. This allows us to identify which tools create new capability regimes and which merely stabilize or accelerate convergence toward faithful formalizations. Finally, to support reproducibility, we will open-source our entire research framework, including the full benchmark, agent implementation, evaluation scripts, and agent tool calling logs upon acceptance. 2. Problem Setting We address the task of formalization: automatically trans- lating natural-language mathematical statements into valid Lean 4 theorem declarations. This task serves as the critical first step in verifying mathematics, bridging the gap between informal human intent and machine-checkable syntax. 1 arXiv:2604.16538v1 [cs.SE] 16 Apr 2026 Tool-Augmented Agents for Lean Formalization Table 1. Benchmark Dataset Composition. DomainSource MaterialN Real AnalysisBasic Analysis (Lebl) (Lebl, 2025a)100 Complex AnalysisCultivating Complex Analysis (Lebl) (Lebl, 2025b) 100 TopologyNotes on Topology (McKay) (McKay, 2025) 100 AlgebraAbstract Algebra (Doty) (Doty, 2025) 100 Total400 2.1. Task Definition Formally, letXbe the space of informal mathematical state- ments andYbe the space of valid Lean 4 source code. Given an inputxâX, the system must generate a formal statementy â Ythat satisfies three criteria: it must pos- sess syntactic validity (compile in Lean 4 with Mathlib), maintain statement-centricity (omitting proofs via:= by sorry ), and ensure semantic faithfulness (logical equiva- lence to x). 2.2. Dataset Construction To benchmark this task, we curated a dataset of 400 graduate-level theorems derived from open-source LaTeX lecture notes and textbooks. We selected sources that pro- vide natural language statements without accompanying formal code, ensuring the task represents a genuine transla- tion effort rather than retrieval. As detailed in Table 1, we balanced the dataset across four major mathematical domainsâReal Analysis, Complex Analysis, Topology, and Algebraâselecting 100 diverse examples from each to ensure broad coverage of mathemati- cal terminology and structures. 2.3. Evaluation Protocol To evaluate the quality of the generated formalizations, we adopt a rigorous two-stage protocol. First, we apply a Com- piler Verification filter; any code that fails to compile is immediately assigned a score of 0. Second, for compiling code, we employ an LLM-as-a-Judge (GPT-5.2 Medium Thinking mode) to assess semantic equivalence. The eval- uator compares the generated Lean statement against the original natural language input and assigns a faithfulness score on a scale of 0â10. Because all reported results de- pend on this judge, we explicitly validate its reliability via cross-judge agreement with an independent model in (Sec- tion 4.5). The judge prompt and rubric (Appendix B) were reviewed and adjusted by a Lean 4âexperienced researcher to align Figure 1. Agent Orchestration Logic. The architecture consists of a central LLM orchestrator (left) and a Lean 4 execution envi- ronment (right). the evaluation with statement-level meaning. Success Metric: We define a generated translationyfor an input statement x as Faithful if and only if: Compiles(y) = True AND EquivalentScore(x,y)⼠9 3. Methodology The agent architecture, illustrated in Figure 1, is structured as a for-loop. The core component is a central LLM orches- trator (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 the consequences of its actionsâsuch as compiler errors or retrieval resultsâbefore deciding on the next step. This design effectively decouples the LLM reasoning from the Lean Compiler verification. 3.1. Tool Definitions We equip the agent with tools designed to bridge the gap between informal mathematical reasoning and formal Lean 4 syntax: â˘Mathlib Retrieval:Retrieval tools such as leaninspectnameallow the agent to ask Lean âwhat is this symbol?â, returning its real type and definition directly from Mathlib. 2 Tool-Augmented Agents for Lean Formalization â˘Expert Drafting: Thelean4translatortool re- quests a translation from the fine-tuned model Herald, providing a specialized starting point. ⢠Compiler Feedback: Theleanreplrunnertool exposes the Lean 4 compiler interface. This provides precise error messages, enabling the agent to iteratively diagnose and correct syntax or validity issues. Detailed specifications of the tool definitions and signatures are provided in Appendix A. 3.2. Prompt Composition To ensure rigorous evaluation, we employ a modular prompt- ing architecture. The system context is dynamically assem- bled from three independent components, ensuring that the core task definition remains constant while we vary the available tools: â˘Role Definition: Instructs the agent to act strictly as a translator, not a prover. The objective is to produce a type-correct theorem statement ending in:= by sorry, ignoring proof generation. â˘General Guidelines: Enforces validity standards, such as requiringimport Mathliband strictly prohibit- ing the invention of new definitions or axioms to pre- vent âhallucinatedâ success. ⢠Tool Specifications: Contains the functional defini- tions for the active toolset. We alter the configuration by simply including or excluding tools from this block, without modifying the instructions above. A common failure mode in agent evaluation is mixing up tool effects with prompt tweaks. If we rewrote the instruc- tions for each tool configuration, any performance difference could come from better prompt wording rather than the tools themselves. To rule this out, we keep the role definition and general guidelines exactly the same in every experiment. The only thing that changes across configurations is the tool interface block (which tools are declared and how they are described). This makes the factorial ablation in Section 5 cleaner: dif- ferences in performance can be attributed to the presence or absence of components such as compiler feedback or expert drafting, rather than to changes in the core instructions. The full prompt templates, including the shared base prompt and all configuration-specific tool-availability blocks, are provided in Appendix A. 3.3. Execution Loop Finally, we formalize the interaction between these compo- nents as a discrete control loop, shown in Algorithm 1. At each stept, the agent receives the current message history (including the modular prompt and any tool outputs) and produces either a tool call or a final response. This process repeats until the Lean compiler reports success or the step budget T max is exhausted. Algorithm 1 Agentic Controller for Lean Formalization 1: Input: Statement x, Context p, ToolSetT 2: H â [SystemPrompt, UserMsg(x,p,Ď )] 3: for t = 1 to T max do 4: Msg â LLM(H) 5: H.append(Msg) 6:if Msg calls TOOL(name,args) then 7:Resultâ ExecuteTool(name,args) 8:H.append(ToolOutput,Result) 9:else if Msg declares SUCCESS then 10:return SUCCESS⡠Compilation Verified 11:end if 12: end for 13: return FAILURE 4. Performance Evaluation To quantify the âagentic premiumâ of our framework, we benchmark the full agent against two static baselines: One- Shot Base (standard GPT-5.2 and Gemini-2.5-Pro prompt- ing without tools) and a One-Shot Fine-Tuned model (Her- ald), which represents the limit of parametric knowledge without execution feedback. 4.1. Performance Analysis Figure 2 presents performance on the 400-theorem bench- mark. One-shot generation without tools proves inade- quate: Herald and GPT-5.2 achieve compilation rates of only 26.0% and 26.2%, respectively. Faithfulness is even lower, ranging from 10.8% (Herald) to 28.0% (Gemini-2.5- Pro). In contrast, the full tool-augmented agent framework (T max = 24) boosts compilation to 89.5% and faithfulness to 60.5%, confirming the value of iterative refinement. 4.2. Efficiency Analysis Beyond raw accuracy, and to provide insight into the bal- ance between cost and performance, we analyze the compu- tational budget required to achieve these results. Figure 3 plots the cumulative success rate against the step budget (T), illustrating the trade-off between performance and cost. The plot reveals two distinct phases in the agentâs behav- ior. We observe rapid convergence up toT = 8, where 3 Tool-Augmented Agents for Lean Formalization HeraldGPT-5.2Gemini 2.5 Pro Agent (Full Framework) 0 20 40 60 80 100 Success Rate (%) 26.0% 26.2% 31.0% 89.5% 10.8% 19.8% 28.0% 60.5% Compiles (Syntax Correct) Faithful (Correct) Figure 2. Main Results. The full framework (all tools enabled; T max = 24) achieves substantially higher compilation and faith- fulness than one-shot baselines on N = 400 theorems. 2510152024 Step Budget (T) 0 10 20 30 40 50 60 Faithful Success Rate (%) Efficiency Analysis: Success Rate vs. Step Budget Agent (Cumulative) GPT-5.2 Baseline (20.3%) Figure 3. Formalization Efficiency. Cumulative faithfulness rate as a function of the inference step budget (T ). nearly half the benchmark is resolved. While returns dimin- ish thereafter, significant gains persist untilT = 14. We therefore identifyT â 14as the practical saturation point, capturing the bulk of solvable problems before computa- tional costs outweigh improvements. 4.3. Domain-Specific Analysis Figure 4 reports domain-level computational overhead under full agent framework, measured by mean and median agent steps (N=100 per domain). Complex Analysis requires the fewest iterations (6.88 mean steps; median 5.0), indicating the lowest computational overhead among the four domains. Real Analysis is the most expensive (9.84 mean steps; me- dian 7.5), with Algebra close behind (9.83 mean; median 6.5). Topology exhibits intermediate overhead (9.20 mean; median 6.0). Appendix C.1 and Appendix C.2 provides the corresponding per-domain summary tables. Complex Analysis Topology Algebra Real Analysis Domain 0 2 4 6 8 10 Steps 6.88 9.20 9.83 9.84 5.00 6.00 6.50 7.50 Domain-level computational overhead (config=111) Mean steps Median steps Figure 4. Domain-level difficulty (config=111). Mean and median agent steps by domain. 4.4. Model Generalizability To verify that the frameworkâs gains are not specific to the GPT-5.2 orchestrator, we evaluate two additional orchestratorsâClaude Sonnet 4.5 and Gemini-2.5-Proâon the full benchmark under the 111 configuration. All three converge to 60â65% consensus faithful despite different one- shot baselines (19â28%), confirming that the dominance of compiler feedback is structural rather than model-specific. Full results are in Appendix C.5. 4.5. Robustness and Metric Validation To validate our LLM-based semantic evaluation, we cross- check the primary judge (GPT-5.2) against another judge (Gemini-2.5-Pro). The two judges exhibit a consistent con- tainment relationship, indicating a structured difference in strictness rather than random disagreement. Judge Containment. Table 2 reports, for each system, the number of translations judged Faithful by each judge. Across all systems, Gemini-2.5-pro consistently accepts more outputs than GPT-5.2, while the consensus is a subset of both. This yields a near-perfect containment pattern Pass Consensus â Pass GPT â Pass Gemini : across all ten configurations, at most 6 out of 400 transla- tions are labeled Faithful by GPT-5.2 but not by Gemini, indicating that Gemini-2.5-Pro is systematically more per- missive, while GPT-5.2 provides a more conservative se- mantic filter. The inclusion relation for the consensus-rate definition is shown in Figure 5. Conservatism of the Primary Metric.We quantify agree- ment using the consensus rate, defined as the fraction of GPT-5.2-labeled Faithful translations that are also labeled Faithful by Gemini: ConsensusRate := #Pass Consensus #Pass GPT . 4 Tool-Augmented Agents for Lean Formalization Table 2. Comparison of LLM judges and their consensus. En- tries count translations that compile and are judged Faithful by each judge; Consensus counts those labeled Faithful by both. SystemGeminiGPT-5.2Consensus One-shot baselines Herald524343 GPT-5.2908179 Sonnet 4.5145116114 Gemini-2.5-Pro122112112 Tool-augmented agents (GPT-5.2 orchestrator) Config 1001129898 Config 001160134132 Config 101174146144 Config 110282241235 Config 111291248242 Config 010304250245 Config 011291251248 Tool-augmented agents (alt. orchestrators, config 111) Sonnet 4.5315271262 Gemini-2.5-Pro307263262 Figure 5. Inclusion relation for faithfulness labels. Across all baselines and tool-augmented agents, the consen- sus rate exceeds 97% in every case, with an overall average of 98.7%. For example, on the full system (111), GPT- 5.2 labeled 248 translations as Faithful, of which Gemini also labeled 242 as Faithful (97.6%). Together with the containment pattern above, this supports using the strict GPTâŠGemini consensus as the primary faithfulness metric throughout the paper (Section 2), providing a conservative lower bound on semantic faithfulness. Where do judges disagree?Figure 6 breaks down GPTâ Gemini disagreements by mathematical domain, aggregated across all ten experimental systems (three one-shot baselines and seven tool-augmented agents). Each domain contains 100 problems evaluated under 10 systems, so each bar sum- marizes 1,000 judged translations. Although overall agreement is high (Section 4.5), the re- maining disagreements are not uniformly distributed across domains. Real Analysis accounts for the largest number of conflicts (125), followed by Algebra (82), Complex Analy- Algebra Complex Analysis Real Analysis Topology 0 20 40 60 80 100 120 140 Total Disagreements 82 61 125 58 GPTGemini Disagreement by Domain Figure 6. GPTâGemini disagreement by mathematical domain. Total number of GPTâGemini disagreements aggregated across all ten experimental systems. sis (61), and Topology (58). This structured concentration suggests that judge disagreements are systematically asso- ciated with particular mathematical domains. This pattern aligns with our domain difficulty results: under the full agent setting (config=111), Real Analysis exhibits the low- est Faithful rate among the four domains (Appendix C, Ta- ble 6), suggesting that harder domains leave more borderline cases for judges to interpret. Human Expert Validation.To directly validate the LLM- as-Judge metric, a Lean 4 expert independently reviewed 138 translations that the consensus metric classified as Faith- ful, scoring each on the same 0â10 rubric. Of 138 scored translations, 83.3% (115/138) received exactly matching scores between the human and LLM judges. A further 14.5% (20/138) disagreed byÂą1within the faithful range (scores of 9 vs. 10), leaving only 3 out of 138 (2.2%) where the human score crossed below the faithful threshold (âĽ9)â all cases where the LLM overestimated (LLM scored 10, human scored 5â7). This yields 97.8% binary agreement on the faithful/unfaithful classification, confirming that the automated metric is well-calibrated with a slight positive bias. We note two limitations of this audit: (1) it covers only outputs classified as faithful (scoreâĽ9), so it measures pre- cision but not recall; and (2) the expert was not blinded to the LLM scores. However, the expert did not uniformly con- firm the LLM labelsâin 3 of 138 cases, substantially lower scores were assignedâsuggesting independent judgment rather than mechanical agreement. A broader audit covering the full score distribution is left to future work. 5 Tool-Augmented Agents for Lean Formalization Table 3. Factorial analysis results. Performance across all2 3 configurations (N = 400), grouped by the presence of the REPL feedback tool (F). We use 0 to denote that tool is turned off. ConfigPerformanceGain TFSComp. (%)Faith. (%)âFaith. (pts) vs . 000 Regime 1: F = 0 (Agent with no REPL) 00026.2519.75â 10030.2524.50+4.75 001 45.5033.00+13.25 10150.0036.00+16.25 Regime 2: F = 1 (Agent with REPL) 11093.5058.75+39.00 11189.5060.50+40.75 010 91.5061.25+41.50 01187.2562.00+42.25 5. Factorial Analysis While the superior performance of the agent is evident, the âblack boxâ nature of the full system obscures which com- ponents drive this success. To disentangle these factors, we conduct a systematic factorial analysis to quantify why the agent succeeds. 5.1. Experimental Design: Factorial Ablation To systematically isolate the contribution of each compo- nent, we decompose the agent arsenal into three tool factors: â˘T (Translation expert). Access to the fine-tuned Her- ald (7B) model for translation. â˘F (Feedback). Access to the Lean compiler feedback loop (REPL) for error correction and compile status. ⢠S (Search).Symbol-retrieval tools (retrieval/web search) for resolving unknown definitions. We adopt a full2 3 factorial design to evaluate interaction effects. We explicitly map the empty-set configuration (â ) to the One-Shot Baseline established in Section 4, as an agen- tic loop with zero tools conceptually reduces to standard autoregressive generation. The remaining seven configura- tions are evaluated by selectively toggling tool definitions in the system prompt. 5.2. Results and Interpretation Table 3 reports performance across all configurations, grouped by the presence of Compiler Feedback (F). To quan- tify 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). Table 4. Factorial main effects on Faithful accuracy. Each effect is computed by Eq. 1. 95% confidence intervals are obtained via bootstrap resampling (B = 10,000). FactorX=1 X=0Effect95% CI Feedback (F)60.628.3+32.3[28.7, 35.9] Search (S)47.941.1+6.8[3.6, 10.0] Translation (T)44.944.0+0.9[â2.1, 4.0] Main-Effect Definition.LetY (T,F,S)denote the Faith- ful accuracy for configuration(T,F,S)in Table 3. For any factor X âT,F,S, its factorial main effect is Effect(X) =E[Y | X=1 ]âE[Y | X=0 ],(1) where the expectation averages uniformly over all settings of the other two factors. Table 4 reports the resulting main effects. â˘Feedback is the capability bottleneck (+32.3pts): Enabling the REPL transforms the agent from a low- success regime (19.75â36.00%) into a high-success regime (58.75â62.00%). This shows that iterative compiler-guided repair is the dominant mechanism enabling faithful Lean formalization. Notably, the mag- nitude of this effect varies by domain, with Complex Analysis benefiting most (+53 pts) and Algebra/Topol- ogy least (+20 pts); see Appendix C.3 for details. ⢠Search is a stabilizer (+6.8pts): Symbol-level re- trieval via#check/#printprovides a consistent boost by reducing hallucinations and improving name resolution, even though it does not create a new per- formance regime on its own. Domain-level analysis (Appendix C.4) shows that Search yields +12.4 pts when full REPL is absent, but near-zero gain (+1.2 pts) when Feedback is enabledâconsistent with the neg- ativeFĂSinteraction (Section 5.3), as full compiler diagnostics subsume symbol-level queries. ⢠Drafting is largely substitutable (+0.9pts): The specialized Herald model yields only a small average improvement. Because the orchestrator (GPT-5.2) is already strong, external drafting becomes redundant once feedback and search are available, and in some cases slightly interferes with the repair loop. 5.3. Interaction Effects: Capability vs. Efficiency Main effects summarize average marginal gains, but they can hide strong regime dependence. To expose when tools improve final faithfulness versus primarily efficiency, we compute simple effects conditioned on the presence of com- piler feedback F . 6 Tool-Augmented Agents for Lean Formalization When does Search improve final faithfulness? Define the Search simple effect at fixed feedback level F =f as â S (F =f ) =E[Y | S=1,F =f ]âE[Y | S=0,F =f ], where the expectation averages uniformly overT. From Table 3, Search yields a large gain without REPL feedback, â S (F =0) = +12.4points, but only a marginal gain with REPL feedback,â S (F =1) = +1.2points. Thus, Search meaningfully improves faithfulness in the low-capability regime (F = 0), but in the high-capability regime (F = 1) it mainly shifts how the agent acquires informationâfrom repeated compileârepair iterations toward earlier, targeted symbol queriesâconsistent with the reduced REPL-call counts in Table 5. When does drafting hurt?Similarly, define the Transla- tor simple effect â T (F =f ) =E[Y | T =1,F =f ]âE[Y | T =0,F =f ], averaging overS. Drafting helps when feedback is absent (â T (F =0) = +3.9points) but hurts when feedback is present (â T (F =1) =â2.0points). This âdrafting penaltyâ suggests that, once compiler-guided repair is available, spe- cialist drafts may become redundant or introduce anchoring effects that impede convergence to the most faithful formu- lation. Substitution captured by interactions. The regime de- pendence above appears as negative interaction terms under the standard difference-in-differences definition (averag- ing over the remaining factor):FĂS =â11.1points and FĂT =â5.9points, whileSĂT â 0. In our implementa- tion, bothF(whole-program compilation) andS(targeted symbol queries) are backed by the same installed Lean/- Mathlib snapshot; in particular,Sis realized via Lean-level checks such as#check/#printrather than an indepen- dent external knowledge source. Under this setup, the nega- tive interactions are consistent with overlapping functional- ity between whole-program diagnostics and symbol-level lookup: when REPL feedback is enabled, enabling Search is associated with only small changes in final faithfulness, while shifting some information gathering from compiler- error-driven trial-and-error toward earlier identifier and type resolution. A domain-level breakdown of this effect is pro- vided in Appendix C.4. Scale and Transfer Effects. A plausible explanation for the limited marginal value of the Expert Drafter (T) is the disparity in model capacity and pretraining diversity. While the Herald translator is fine-tuned on Lean data, the orches- trator (GPT-5.2) is trained at much larger scale on a broad mixture of programming languages, mathematics, and nat- ural language. This large-scale, multi-domain pretraining Table 5. Tool Usage Counts (Total). Cumulative tool invoca- tions across the subset with complete tool-call logs (N = 384; all accuracy results useN = 400). We report REPL calls (lean4replrunner) and aggregate symbol-retrieval tools intoS total = searchonline + leaninspectname + leanresolvename. (T, F, S)Trans.REPL S total Notes (0,1,0)014960Feedback-only (0,1,1)010501726+Search (REPLâ) (1,1,0)25713740Feedback + Expert (1,1,1) 11210081913+Search (REPLâ) enables strong cross-domain transfer, whichâwhen com- bined with compiler feedback and retrievalâallows the generalist model to adapt to Lean syntax and semantics through iterative correction, reducing the marginal value of a domain-specialized draft. The value of verification beyond retrieval. Search pro- vides symbol-level semantic primitives (existence checks, types, and definitions via#check/#print), but it does not provide whole-statement verification or full elaboration diagnostics. In contrast, Feedback adds (i) a global compi- lation/elaboration signal and (i) actionable error messages that enable iterative repair, which appear to be the dominant drivers of faithful formalization. 5.4. Behavioral Analysis: REPL Efficiency While the factorial analysis in Section 5.2 identifies which tools determine final Faithful accuracy, tool invocation logs provide complementary insight into how efficiently the agent reaches that accuracy. In particular, the number of calls to the Lean REPL (lean4replrunner) serves as a proxy for the amount of trial-and-error required to obtain compilable and faithful Lean code. As shown in Table 5, using the convention(T,F,S), adding Search reduces REPL usage in bothT = 0andT = 1 settings when feedback is enabled. ForT = 0, REPL calls drop from 1,496 in (010) to 1,050 in (011), a 29.8% reduction. ForT = 1, REPL calls drop from 1,374 in (110) to 1,008 in (111), a 26.6% reduction. Meanwhile, Search usage increases substantially (from 0 to 1,726 or 1,913), indicating that the agent shifts effort from expensive compile-and-repair iterations toward cheaper symbol-level validation. One plausible mechanism is that, before Search is avail- able, the agent may rely on REPL feedback not only for âcompile/no-compileâ verification but also largely to infer missing identifiers, expected variables, and type constraints from Leanâs error messages; introducing Search could re- duce this reliance by providing symbol-level information 7 Tool-Augmented Agents for Lean Formalization earlier. Finally, we note that the extensive interaction logs gener- ated by our agent constitute a valuable dataset of successful and failed formalization trajectories. These traces map the trial-and-error process of resolving compiler errors, making them an ideal corpus for future research into Reinforcement Learning (RL) for formalization. By training on these repair loops, future models might internalize the feedback dynam- ics, learning to predict successful repairs without incurring the high inference cost of the live REPL. 6. Limitations Our study has several important limitations that contextual- ize the interpretation of the results. Statement Fidelity vs. Provability.Our task is translating natural language into valid Lean 4 statement declarations (ending in:= by sorry). We enforce syntactic validity and semantic faithfulness but do not verify provability. In a small pilot on 12 benchmark problems, Aristotle achieved 11/12 faithful translations by consensus, while our agent achieved 8/12 on the same subset using general-purpose LLMs. A systematic comparison with Lean-specialized models remains future work. Dependence on the Lean Environment. In our cur- rent implementation, all formal feedback ultimately flows through the Lean 4 environment, either directly via REPL compilation or indirectly through symbol-level queries backed by the installed Mathlib snapshot. As a result, our factorial analysis primarily reflects differences in interaction modality (whole-program compilation vs. targeted symbol lookup) rather than access to fundamentally independent sources of mathematical truth. A natural extension is to build a static, agent-facing Mathlib dataset (e.g., indexed statements, docstrings, and symbol metadata) that supports offline lookup and reduces reliance on the live REPL during search. However, this direction in- troduces its own limitation: Mathlib evolves rapidly, so any fixed dataset can become stale, potentially yielding outdated names, moved theorems, or changed type signatures unless it is versioned and regularly refreshed. Restricted Mathematical Coverage. Our benchmark covers four major domains (Real Analysis, Complex Analy- sis, Topology, Algebra). We caution that these results may not generalize to combinatorial or discrete domains (e.g., Graph Theory, Number Theory), where formalization re- lies less on structural type definitions and more on intricate logical predicates. Compute Cost. Agentic formalization is significantly more expensive than one-shot generation. Although symbol search tools reduce the number of compiled iterations, the inference cost of the full REPL loop remains a barrier to real-time interactive assistance. 7. Conclusion We presented a systematic study of tool-augmented agents for translating natural-language mathematics into Lean 4. By combining a generalist LLM with retrieval, expert draft- ing, and compiler feedback, the agent raises faithfulness from 28.0% to 60.5% over the strongest one-shot baseline on a new 400-theorem benchmark. Beyond raw performance, our factorial analysis reveals a clear structural picture. Compiler feedback is the domi- nant capability driver, enabling a transition from unreliable drafts to consistently faithful formalizations. Symbol-level search improves efficiency and stability by reducing hallu- cinations and lowering the number of expensive compileâ repair cycles, while expert drafting provides only marginal gains once feedback and search are available. These results demonstrate that execution and retrieval, rather than para- metric specialization alone, are the critical ingredients for scalable mathematical formalization. Together, these findings suggest a general design principle for formal reasoning agents: high-precision execution en- vironments should serve as the primary scaffold for LLM reasoning, with retrieval used to stabilize and accelerate con- vergence. Our results suggest a broader lesson: for rapidly evolving formal libraries, one-off fine-tuning on a static cor- pus may be brittle, and sustained progress likely depends more on verification-coupled iteration (and continual re- fresh) than on a fixed offline drafter alone. We believe this paradigm will be central to future systems that aim to bridge informal mathematical knowledge and machine-verifiable proof. Impact Statement This work advances methods for translating informal math- ematics into formal proof assistant statements. Potential impacts include improving reliability and accessibility of formal verification tools. Risks include overreliance on auto- mated formalization and evaluation bias; we advocate trans- parent reporting of tool configurations and failure modes. References Castelvecchi, D. AI models solve maths problems at level of top students. Nature, 644:7, 2025. de Moura, L. and Ullrich, S. The Lean 4 theorem prover 8 Tool-Augmented Agents for Lean Formalization and programming language (system description). In Automated Deduction â CADE 28, volume 12699 of LNCS, p. 625â635. Springer, 2021. doi: 10.1007/ 978-3-030-79876-537. Doty, S. R. Lecture notes on abstract algebra.https:// github.com/srdoty/AbstractAlgebraBook, 2025. GitHub repository; accessed 2025-09-04. Gao, G., Wang, Y., Jiang, J., Gao, Q., Qin, Z., Xu, T., and Dong, B. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Conference on Learning Representations, 2025. LeanProverCommunity.Missingunder- graduatemathematicsinMathlib.https: //leanprover-community.github.io/ undergrad_todo.html. Accessed: September 4, 2025. Lebl, J.Basic analysis: Introduction to real analy- sis.https://github.com/jirilebl/ra, 2025a. GitHub repository; accessed 2025-09-04. Lebl, J. Guide to cultivating complex analysis: Working the complex field.https://github.com/jirilebl/ ca, 2025b. GitHub repository; accessed 2025-09-04. McKay, B. Topology lecture notes.https://github. com/Ben-McKay/topology-lecture-notes, 2025. GitHub repository; accessed 2025-09-04. Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., et al. Kimina-prover preview: Towards large formal reason- ing models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025. 9 Tool-Augmented Agents for Lean Formalization A. Agent Implementation Details A.1. Prompt Assembly The system prompt is constructed from three modular components: (i) a task definition establishing the core translation objective, (i) a general usage guide containing fixed best practices for Lean 4 code generation, and (i) 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 i) fixed, while selectively enabling or disabling external tools (i) to isolate the causal effect of each capability. We assemble (i) and (i) into a Shared Base Prompt, shown below, while the capability block definitions are provided in Appendix A.3. A.2. Shared Base Prompt Base System Prompt You are an expert Lean4 translation agent. Your task is to translate a natural-language mathematical statement into faithful Lean4 syntax (NOT a proof). The final result must: - import Mathlib at the very top - compile in Mathlib - be semantically faithful to the original statement - end with â:= by sorryâ You are NOT proving anything. You are only producing a correctly typed, correct-meaning Lean statement. GENERAL INSTRUCTIONS FOR CODE GENERATION ⢠The Lean file MUST start with: import Mathlib ⢠The Lean file MUST contain exactly ONE final translated statement representing the original natural-language meaning. ⢠The final statement MUST end with: := by sorry ⢠Do NOT write any proof code before â:= by sorryâ (no âbyâ, âsimpâ, âhaveâ, âcalcâ, etc. anywhere before the final â:= by sorryâ). ⢠Do NOT invent new definitions, axioms, constants, or placeholder structures. ⢠Prefer robust formulations: use quantifiers, membership, andâcharacterizations rather than fragile definitional equalities. ⢠Only finish when the last written version: (1) compiles in Mathlib (if lean4replrunner is available) (2) is semantically faithful to the original statement When both are satisfied, return: âstatusâ: âsuccessâ A.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 theAVAILABLE TOOLSblock 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. Tool Block (T=1, F=1, S=1) AVAILABLE TOOLS lean4translator(statement) Draft a Lean 4 statement using the fine-tuned Herald translator (you may edit or ignore). leanwritefile(code) Write the full Lean file to the workspace (imports + exactly one final statement). lean4 replrunner() Compile the current Lean file and return compiler feedback. leaninspectname(name, imports?, includeprint?) Query Mathlib about an identifier via #check/#print. leanresolvename(token, namespacehints?, imports?, topk?) Suggest likely Mathlib identifiers for an unknown or ambiguous token. 10 Tool-Augmented Agents for Lean Formalization searchonline(query) Run a web search and return results for the query. A.4. Tool Interfaces Agent Tool API ToolArgumentsFunctionality leaninspectname name,imports?, includeprint? Checks whether a Mathlib symbol exists and re- turns its type (#check) and optionally its definition (#print). leanresolvename token,namespacehints?, imports?, topk? Performs fuzzy symbol resolution to map informal or incorrect names to valid Mathlib identifiers. lean4 replrunner Lean 4 code to be executed Compiles the current Lean file and returns compiler diagnostics (errors, warnings, and success flags). lean4translator statementInvokes the fine-tuned Herald translator to generate a draft Lean formalization of the natural-language input. search online queryPerforms external web search to retrieve mathemati- cal or documentation context not present in Mathlib. A.5. Example Execution Trace Example Execution Trace (agent tool calls) StepToolArguments (agent side) 1 leanwritefile path="jirileblcaca17658.lean";content = import Mathlib ... theorem jirilebl caca17658 ... := by sorry 2 lean4 replrunner path="jirileblcaca17658.lean" 3 leaninspectname name="Polynomial.IsConstant" 4 leaninspectname name="Polynomial.eval" 5 leaninspectname name="Polynomial.isConstant" 6 lean inspectname name="Polynomial.natDegree" 7 leanwritefile path="jirileblcaca17658.lean";content = patched theorem uses p.natDegree ̸= 0 and Polynomial.eval 8 lean4replrunner path="jirileblcaca17658.lean" B. LLM-as-a-Judge Prompt and Rubric We evaluate semantic faithfulness using an LLM-as-a-judge that receives: (i) the natural-language statement, (i) the generated Lean 4 code, and (i) a booleancompilepass. The judge outputs a JSON object with fieldsfaithfuland grade(0â10). Ifcompilepass=false, we requirefaithful=falseand restrict the grade to 0â3. The translation is considered as faithful if and only if the code compiles and the score is >= 9. Judge system prompt (verbatim) You are an expert in Lean 4, Mathlib, and mathematics. You are judging TRANSLATION-ONLY.,â 11 Tool-Augmented Agents for Lean Formalization 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 <short explanation focusing on statement-level comparison> ### END THOUGHT",â Return ONLY valid JSON. No extra keys. No markdown outside JSON. 12 Tool-Augmented Agents for Lean Formalization C. Additional Domain Results C.1. Domain Metrics under Full Configuration Domain metrics under config 111 Table 6. Domain metrics under config=111. Conditional faithfulness is computed as Faithful/Compile. DomainCompile Faithful FaithfulâCompile Steps (mean) Steps (median) Complex Analysis0.950.820.866.885 Real Analysis0.890.490.559.847.5 Algebra0.870.560.649.836.5 Topology0.870.610.709.206 C.2. Judge Scores by Domain Average judge scores by domain across configurations Table 7. Average faithfulness scores by domain and configuration. Columns correspond to tool configurations in(T, F, S)bit order. Domain001010011100101110111 Algebra5.60 7.14 7.23 4.46 5.85 7.20 7.22 Complex Analysis 4.72 9.27 8.91 4.20 4.94 8.94 8.98 Real Analysis4.62 7.38 7.34 3.59 4.75 7.33 7.31 Topology5.39 7.10 7.03 4.47 6.14 7.05 7.25 Interpretation. Score trends are consistent with the domain difficulty ranking in Section 4.3: Complex Analysis attains the highest scores under tool-enabled settings, while Real Analysis remains lowest. C.3. Domain-Level Feedback Effects 001010011100101110111 Algebra Complex Analysis Real Analysis Topology domain 0.410.560.580.280.430.570.56 0.280.840.800.250.310.790.82 0.270.540.560.160.260.510.49 0.380.560.570.290.460.540.61 pivot_domain_faithful 0.2 0.3 0.4 0.5 0.6 0.7 0.8 Figure 7. Faithful rate by domain and configuration. 13 Tool-Augmented Agents for Lean Formalization Domain-wise effect of Compiler Feedback (F) DomainF=0 (avg)F=1 (avg)âF Complex Analysis0.280.81+0.53 Real Analysis0.230.53+0.30 Algebra0.370.57+0.20 Topology0.380.57+0.19 Interpretation. Complex Analysis benefits most from compiler feedback (+53 pts), likely due to mature Mathlib coverage. Algebra and Topology show smaller gains ( +20 pts), suggesting either limited library support or intrinsic formalization difficulty. C.4. Domain-Level Effects of Search (S) Simple effect of Search conditioned on Feedback The Search tool (S) provides symbol-level queries via#check/#print, accessing a subset of REPL functionality without full compilation diagnostics. As noted in Section 5.3, both tools are backed by the same Lean/Mathlib snapshot, leading to the negative interaction FĂS =â11.6 pts. F=0F=1 DomainS=0S=1S=0S=1 Algebra0.280.420.5650.57 Complex Analysis0.250.300.8150.81 Real Analysis0.160.270.5250.525 Topology0.290.42 0.550.59 Avg âS+10.8 pts+1.0 pts Interpretation. When full REPL is unavailable (F=0), symbol queries provide substantial gains (+10.8 pts average). Once full REPL is enabled (F=1), the marginal benefit of Search drops to near zero (+1.0 pts), confirming that whole-program diagnostics subsume symbol-level information. This domain-level breakdown corroborates the negativeFĂSinteraction reported in Section 5.3. C.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-theorem benchmark under the 111 (all tools) configuration. 14 Tool-Augmented Agents for Lean Formalization GPT-5.2Sonnet 4.5Gemini 2.5 Pro 0 20 40 60 80 100 Success Rate (%) 89.5% 93.0% 80.5% 60.5% 65.5%65.5% Compiles (Syntax Correct) Faithful (Correct) Figure 8. Multi-model agent comparison (config 111). All three orchestrators converge to 60â65% consensus faithful despite different one-shot baselines (19â28%). As shown in Figure 8, all three models show large uplift from the tool-augmented framework (+148 to +163 faithful translations) and converge to 60â65% consensus faithful despite markedly different one-shot baselines (19â28%). This convergence confirms that the findings of the factorial analysisâparticularly the dominance of compiler feedbackâare structural rather than model-specific. 15