1 Introduction↩︎

Autoformalization translates informal mathematics into Lean statements that compile and preserve the intended mathematical claim. Yet the task is naturally many-to-many: the same theorem can often be encoded as multiple faithful Lean statements, while standard single-output protocols collapse this structure into one generated statement. For downstream proving, that granularity is too coarse. A formal statement is not merely a translation endpoint; it is the prover-facing interface through which proof search is attempted under a fixed prover and attempt budget. Compilation requires successful elaboration and type checking under the chosen context, while semantic faithfulness remains a separate requirement. As large language model provers become more capable [1]–[4], structural choices in the statement itself increasingly affect downstream proof search.

Semantic consistency therefore does not imply prover equivalence: by prover equivalence we informally mean comparable proof-search behavior under the same prover and attempt budget. A formal statement that compiles and preserves the intended claim is not necessarily a prover-friendly target; faithful variants can differ substantially in proof-search cost and success rate. 1 illustrates this gap: candidates that pass compilation and semantic checks can still lead to different prover outcomes under the same prover protocol. A single generated statement therefore discards prover-relevant variation. This motivates a repertoire view: the search procedure should construct multiple faithful Lean statements that expose different proof-search behavior under the same prover budget.

We formulate autoformalization as a budgeted test-time search problem. Under a generator-call budget, the system must construct a repertoire of candidate formalizations that are compilable, semantically consistent, and useful for downstream proving. This requires preserving compilation feasibility, avoiding semantic drift, and introducing structural diversity, without burning budget on a handful of easy problems or near-duplicates.

To address these requirements, we propose FormalEvolve, a compilation-gated neuro-symbolic evolutionary framework built around an archive search protocol. FormalEvolve maintains a compilation-feasible archive of candidate Lean statements and expands it primarily through LLM-driven mutation, crossover, and bounded patch repair. In addition, conservative generator-call-free AST rewrites act as a structural diversification fallback when patching stalls, for example after repeated duplicates or compile failures. Usage penalties and duplicate-aware selection encourage the search to cover more problems and statement forms. 2 gives a high-level overview.

Under a generator-call budget of \(T{=}100\), FormalEvolve reaches SH@100 of 58.0% on CombiBench and 84.9% on ProofNet, improving over all no-archive controls on both benchmarks while reducing the cross-problem concentration of semantic successes. Under a fixed \(B{=}64\) prover budget, the resulting repertoires improve theorem-complete downstream proving over the matched no-archive control on both benchmarks. To separate repair-model strength from archive search, we include a matched hybrid control that uses the same stronger repair model without an archive; FormalEvolve still gains at the statement stage. The pattern also holds in a stronger-base statement-generation setting. Because semantic labels come from an LLM judge, we also provide manual audits at both the statement and theorem-complete stages to calibrate the evaluation.

More broadly, FormalEvolve illustrates a verifier-gated diversity-search pattern: when many valid formal artifacts can express the same informal intent, test-time compute can construct a repertoire of useful alternatives under hard checker feedback.

We make three primary contributions:

1. Problem Modeling and Protocol: We formulate Lean 4 autoformalization as budgeted test-time repertoire search and introduce budget-auditable metrics that connect statement-level coverage, cross-problem concentration, and downstream proving performance.

2. Search Mechanism: We propose FormalEvolve, a compilation-gated neuro-symbolic evolutionary framework that combines archive-based LLM mutation and crossover, bounded patch repair, and generator-call-free symbolic AST rewrites.

3. Empirical Evidence: We show that FormalEvolve improves semantic hit rates and cross-problem coverage uniformity under fixed generator-call budgets, improves theorem-complete downstream proving over a matched no-archive control by constructing diverse candidate repertoires, and preserves statement-stage archive-search gains under a stronger-base setting.

2 Related Work↩︎

2.0.0.1 Autoformalization and semantic evaluation.

Large language models have enabled autoformalization at scale, with systematic evaluation on curated formal-mathematics benchmarks [5]–[7]. Reliability remains a central bottleneck: compilation checks syntax and elaboration, but is only a weak proxy for semantic consistency, motivating dedicated semantic judges and alignment evaluators [8], [9]. Recent systems further improve semantic fidelity by interleaving iteration, tool feedback, and grounding [3], [10]–[12]. These lines of work primarily improve or assess individual formalizations within a single-output view. We study fixed-budget construction of semantically consistent and diverse candidate repertoires.

2.0.0.2 Statement variation and prover utility.

For downstream proving, a formal statement serves both as a semantic target and as the object consumed by a prover. Even among semantically consistent candidates, minor, semantics-intended reformulations can substantially change proof-search difficulty [13]. At the same time, semantic evaluation itself is imperfect and can disagree with downstream prover behavior [10]. These observations motivate treating autoformalization as a fixed-budget repertoire-construction problem, where multiple faithful candidates expose different prover utilities. Such a repertoire mitigates prover sensitivity by exposing several semantically aligned targets under the same fixed budget.

2.0.0.3 Test-time search and quality-diversity.

Test-time search and evolutionary optimization with LLMs have been explored for sample-efficient program and algorithm improvement [14]–[16]. Quality-diversity methods construct repertoires of high-quality solutions [17], [18], and multi-criteria evolutionary optimization provides a complementary perspective on multiple objectives [19]. EvolProver evolves formalized problems via symmetry and difficulty, including semantics-preserving AST rewrites, to augment training data for provers [20]. For Lean statement search, elaboration and type checking define the feasible set: a candidate must compile before it can enter the archive or be reused as a parent. For each informal problem, FormalEvolve builds a test-time repertoire of candidate statements used for that problem’s evaluation and downstream proving. EvolAST-style conservative rewrites are used only as a generator-call-free fallback for structural diversification when LLM patching stalls.

3 Method↩︎

FormalEvolve instantiates the shift from single-output prediction to many-to-many repertoire construction as per-problem test-time search over Lean 4 statement candidates under a generator-call budget \(T\) ([sec:budget]). Given an informal statement \(x\), the goal is to construct a deduplicated repertoire of candidates that compile and pass the semantic judge within budget. The search starts from a small compilation-feasible seedbank, stores unique compiled candidates in an archive, and expands it through LLM patching, bounded repair, and call-free EvolAST diversification. Because Lean compilation defines a narrow feasible region, archive entry is compilation-gated, near-feasible candidates are salvaged by bounded repair, and lightweight diversity operators reduce collapse. Our reported output is the deduplicated semantically consistent repertoire generated within budget, i.e., candidates satisfying \(\mathsf{Comp}(c){=}1\) and \(\mathsf{Sem}(c){=}1\), which we use for SH@T and downstream proving.

3 summarizes the same loop and makes the two domain gates explicit: \(\mathsf{Comp}\) checks whether a candidate passes Lean 4 compilation, while \(\mathsf{Sem}\) is the semantic-faithfulness judge against the informal theorem \(x\). The counter \(t\) tracks debited generator calls, \(\mathcal{A}_I\) is an island archive, \(\mathcal{Z}\) denotes sampled prompt context and inspirations, \(\mathcal{B}\) is the candidate batch produced by proposal and bounded repair, and \(\mathcal{G}\) is the persistent accepted repertoire returned at the end. 2 gives the visual overview, and 11.1 gives the detailed pseudocode.

3.1 Search Procedure and State↩︎

3.1.0.1 Basic objects and gates.

We search over Lean 4 candidates of the form \(c=(\hat{h},y)\), where \(\hat{h}\) is an import/header context and \(y\) is the primary Lean 4 statement or declaration target. Most candidates are theorem/lemma-style files with placeholder proofs, but benchmark contexts and model outputs can also contain def, abbrev, or example templates; for this reason, the prover-stage evaluation separately reports theorem-complete success for explicit theorem/lemma completions. We evaluate candidates using a compilation predicate \(\mathsf{Comp}(c)\in\{0,1\}\) and a semantic predicate \(\mathsf{Sem}(c)\in\{0,1\}\) (instantiated by an LLM judge in 4). Compilation is a hard feasibility gate: only candidates with \(\mathsf{Comp}(c)=1\) are eligible to enter the archive and be reused as parents/inspirations. We treat compilation/elaboration as verifier feedback: it both defines feasibility and provides the primary error feedback for bounded compilation repair. During search, the archive stores unique compilation-feasible candidates regardless of \(\mathsf{Sem}(c)\) (i.e., it may include semantically inconsistent stepping stones) and is used only for parent/context sampling. For reporting SH@T and downstream proving, we define the semantically consistent repertoire as the deduplicated set of candidates generated within budget that satisfy both \(\mathsf{Comp}(c)=1\) and \(\mathsf{Sem}(c)=1\). FormalEvolve uses these two predicates during test-time search and bounded repairs; downstream proving is evaluated only when reporting proof utility. All generator-side LLM calls (seeds, patches, and repairs) are debited against the same per-problem generator-call budget \(T\) ([sec:budget]).

3.1.0.2 Seedbank initialization.

We initialize the search by sampling a small seedbank with a seed model \(M_{\mathrm{seed}}\), evaluating each seed with the compiler and semantic judge, and inserting the compilation-feasible subset into the archive. When a pre-sampled seedbank is reused across methods, we still debit each reused seed as one generator call to preserve consistent accounting. We separate the seed and patch roles: \(M_{\mathrm{seed}}\) provides initial candidates, while \(M_{\mathrm{patch}}\) performs edit-conditioned proposals and bounded repairs. Concrete model choices are specified in 4.

3.1.0.3 Archive, islands, and duplicates.

We maintain a per-problem archive \(\mathcal{A}\) of unique compilation-feasible candidates that serves both as a parent pool and as prompt context. We use an island model with \(K\) semi-isolated archive populations (default \(K=2\)). When \(K=1\), FormalEvolve uses a single archive population: it still retains archive-based parent reuse, archive-conditioned context sampling, usage-penalized selection, and bounded repair, but removes island partitioning and migration. Each iteration samples one island and restricts parent/context sampling to it. In the main configuration, migration occurs every 10 generations at rate 0.1 with the top candidate in each island protected. Detailed hyperparameters are provided in [sec:appendix-config,sec:appendix-impl-islands]. Exact duplicates under canonicalization (whitespace/name normalization) are rejected at archive insertion to reduce collapse. In 3, SampleParent uses the scoring rule defined below, and \(n_i\) tracks how often \(c_i\) has already been selected as a parent.

3.1.0.4 Scoring and usage-penalized selection.

The selection rule separates archive storage from parent sampling. Storage is purely feasibility-gated: only candidates with \(\mathsf{Comp}(c)=1\) can enter the archive, and the archive retains all unique compilation-feasible candidates. This matters because different faithful statements can expose different binder structures, imports, and theorem shapes to the downstream prover. Scores therefore bias reuse as future parents; archive contents remain available for later sampling, and proof utility is evaluated downstream under the fixed prover protocol.

For an archived candidate \(c_i\in\mathcal{A}_I\), let \(n_i\) be how many times it has already been selected as a parent. We assign each candidate a sampling weight \(w_i\) and sample proportionally: \[\Pr(p=c_i\mid\mathcal{A}_I) = \frac{w_i}{\sum_{c_j\in\mathcal{A}_I} w_j}. \label{eq:parent-sampling}\tag{1}\] The weight combines the gate score and a usage discount: \[\begin{align} s_i &= \mathsf{Comp}(c_i)(1+\mathsf{Sem}(c_i)),\\ \tilde{s}_I &= \mathrm{median}_{c_j\in\mathcal{A}_I}(s_j),\\ d_I &= \max(\mathrm{MAD}(\{s_j:c_j\in\mathcal{A}_I\}),\varepsilon),\\ z_i &= (s_i-\tilde{s}_I)/d_I,\\ u_i &= [1+(1+\beta)n_i]^{-1},\\ w_i &= \sigma(\lambda z_i)u_i . \end{align} \label{eq:parent-weight}\tag{2}\] Since archived candidates already compile, \(s_i=1\) for judge-negative archive members and \(s_i=2\) for judge-consistent members. \(u_i\) is a usage discount: it equals 1 for a never-used parent and decreases as the same parent is sampled repeatedly. We set \(\varepsilon=10^{-6}\) only to avoid division by zero when all scores are identical, and use \(\lambda=10\) and \(\beta=0.05\) in the main runs.

3.2 Proposal, Repair, and Diversification↩︎

3.2.0.1 Variation operators.

Given a selected parent, the patch model proposes a new candidate using one of three prompt templates. Full patching rewrites the entire statement (and, when allowed, its surrounding imports) conditioned on the informal input and parent context. Diff patching performs localized edits that make minimal changes relative to the parent, guided by compiler/judge feedback. Cross patching additionally conditions on one or more inspiration candidates sampled from the current archive, and asks the model to combine useful elements (e.g., import context, binder structure, or type annotations) while preserving the informal input’s meaning (see 12 for prompt details and 10 for audited examples). All three templates return a complete Lean 4 file (imports plus a single statement) and are budgeted identically as generator calls.

3.2.0.2 Bounded compilation and semantic repair.

We compile the full Lean 4 file and treat successful compilation as a hard feasibility gate. When compilation fails, FormalEvolve invokes a repair prompt that proposes a minimal patch conditioned on compiler feedback. Repair is bounded to a fixed cap of two repair attempts per proposal path in the main configuration; each attempt is debited as a generator call, and repair stops immediately when the remaining budget is exhausted. Bounding repair makes the search budget-auditable under hard cutoffs and prevents pathological cases where a single hard candidate consumes most of the call budget. For a compilable candidate that fails the semantic judge (\(\mathsf{Comp}(c)=1\) and \(\mathsf{Sem}(c)=0\)), we optionally apply a bounded semantic repair stage by prompting \(M_{\mathrm{patch}}\) to revise the statement conditioned on the informal input and the judge’s rationale (when available), and then re-evaluate; all repair and semantic-repair attempts are debited. We view compilation repair and semantic repair as two instantiations of the same edit-conditioned patch mechanism, differing only in the feedback source (compiler errors vs.judge rationale).

3.2.0.3 Call-free diversity fallback (EvolAST).

Archive-based search can suffer from mode collapse where many candidates become near-duplicates or exploit superficial patterns. FormalEvolve mitigates this primarily via the usage penalty in parent sampling. We additionally apply a conservative, generator-call-free AST rewrite fallback inspired by EvolProver [20] when patching stalls (e.g., repeated duplicates or compile failures). In the reported runs, each triggering proposal contributes at most one EvolAST representative, and EvolAST outputs are not recursively rewritten or sent into LLM repair. EvolAST rewrites only within binder types and the goal type (imports/preamble unchanged) to produce symmetry/structure variants, which are then filtered by the same compilation gate and semantic judge. Thus EvolAST is free only with respect to generator calls; its compilation and judge overhead is reported separately in 11.2.

4 Experiments↩︎

4.0.0.1 Benchmarks.

We evaluate on ProofNet [6] (Lean 4 port; test split, \(N{=}186\)) and CombiBench [21] (\(N{=}100\), domain/style shift).

4.0.0.2 Environment.

Candidates are compiled under a pinned Lean 4/Mathlib toolchain served by Kimina Lean Server [22]; full details are in 11.3.

4.0.0.3 Budget.

We use a generator-call budget \(T=100\) per problem, debiting each proposal or bounded repair LLM call as one call; repair/semantic-repair attempts are debited as separate calls. Compilation checks, semantic-judge calls, and EvolAST-triggered candidate evaluations are evaluator-side costs. Generator-call counts include seed, proposal, and repair LLM calls; Appendix 11.2 audits judge-call overhead and EvolAST-attributed judge calls.

4.0.0.4 Baselines.

Our sampling baselines instantiate a memoryless, no-archive setting: budget-matched variants with fresh sampling/repair and no archive state. They include Sample (no repair), Compile Repair (bounded compilation repair), and Compile+Semantic Repair (compilation repair plus one bounded semantic-repair call for compilable candidates failing the judge). To separate archive-search effects from patch-model strength, Table 1 also reports Hybrid control: the same Kimina-generation/Qwen3-repair stack under \(T{=}100\), but with independently sampled trajectories and no archive state, parent reuse, archive context, usage-penalized selection, or island migration.

4.0.0.5 Models.

In our main runs, the sampling baselines use Kimina-Autoformalizer-7B for sampling/repair, while FormalEvolve uses Kimina-Autoformalizer-7B for seeding and Qwen3-30B-A3B for patch/repair. For proof utility, we fix the prover to Goedel-Prover-V2-32B [23] with a fixed prompt template ([sec:appendix-prover-prompt]).

4.0.0.6 Search configuration.

Unless stated otherwise, FormalEvolve uses \(K=2\) islands, archive capacity 40, parent-selection parameters \(\lambda=10\) and \(\beta=0.05\), an operator mix of full/diff/cross patching with probabilities 0.5/0.3/0.2, and migration every 10 generations at rate 0.1; Appendix 11.3 gives the complete configuration.

4.0.0.7 Metrics.

CH@T and SH@T denote the fraction of problems with at least one compilable candidate (resp.at least one compilable, judge-consistent candidate) within \(T\) debited generator calls. Coverage alone leaves open whether additional semantic successes are broadly distributed or concentrated on a small set of already-easy problems. Let \(s_j(T)\) be the number of generated candidates with \(\mathsf{Comp}(c)=1\) and \(\mathsf{Sem}(c)=1\) for problem \(j\) within budget \(T\); we therefore report cross-problem concentration via the Gini coefficient \[\mathrm{Gini}(T)=\frac{\sum_{i=1}^{N}\sum_{j=1}^{N} |s_i(T)-s_j(T)|}{2N\sum_{j=1}^{N} s_j(T)+\varepsilon},\] with the same numerical stabilizer \(\varepsilon=10^{-6}\) used in parent-score normalization. We also report the Top-10% share \(\sum_{j\in \mathrm{Top}_{10\%}} s_j(T)/\sum_{j=1}^{N} s_j(T)\) (where \(\mathrm{Top}_{10\%}\) selects the problems with the largest \(s_j(T)\)). We evaluate downstream proof utility under a fixed \(B=64\) prover protocol (pass@64 / complete@64 / theorem-complete@64; 2); full definitions are in 7.1.

4.0.0.8 Semantic judge and manual calibration.

The semantic predicate \(\mathsf{Sem}\) is implemented by CriticLean-Qwen3-14B with a fixed prompt and serving configuration; the judge prompt and judge-call accounting are reported in Appendix 12.4 and Appendix 11.2. Our semantic metrics rely on an LLM-as-judge implementation of \(\mathsf{Sem}\); we therefore include manual faithfulness audits for both a statement-stage sample from judge-positive ProofNet outputs and a theorem-complete prover-stage sample produced under the fixed \(B=64\) prover protocol. We summarize these audits in 5 and provide the protocol and tables in Appendix 9.1.

5 Results↩︎

5.1 Coverage and Uniformity↩︎

5.1.0.1 Statement generation at \(T=100\).

Table 1 reports statement generation under the same \(T=100\) generator-call budget, including coverage (CH/SH) and concentration (Gini/top-10% share). Against the hybrid no-archive control, which uses Kimina generation with the same Qwen3 repair model but no archive, FormalEvolve increases SH@100 from 0.530 to 0.580 on CombiBench and from 0.828 to 0.849 on ProofNet. We therefore interpret coverage together with cross-problem concentration and downstream proof utility.

5.1.0.2 Ablations and component effects.

The strongest Kimina-only baseline is Compile+Semantic Repair. Adding the stronger Qwen3 repair model without an archive already improves SH@100 from 0.460 to 0.530 on CombiBench and from 0.780 to 0.828 on ProofNet. FormalEvolve then adds archive-based search on top of this repair strength, so the hybrid row can be read as a matched no-archive ablation. Removing patch repair drops SH@100 from 0.580 to 0.470 on CombiBench and from 0.849 to 0.780 on ProofNet, identifying bounded repair as the largest direct driver of SH@100. The archive then makes repaired candidates reusable as parents and prompt context, allowing local repair gains to propagate through later search steps while reducing repeated edits of the same templates. The island and EvolAST ablations are smaller and dataset-dependent under the fixed budget: \(K{=}1\) removes only island separation, remaining an archive-based single-population search, and it improves ProofNet coverage and concentration as well as CombiBench concentration. The default \(K{=}2\) setting gives the strongest CombiBench SH@100 among FormalEvolve variants and is used for downstream proof evaluation. Accordingly, the island rows are reported as implementation sensitivity; the main controlled comparison remains archive-based search versus matched no-archive controls.

None

5.1.0.3 Cross-problem concentration.

Coverage alone can hide a failure mode in which a method spends most of its successful calls on the same easy problems. We therefore report Gini and top-10% share over per-problem semantic_ok counts. The default FormalEvolve configuration lowers both concentration metrics relative to the hybrid control: on CombiBench, Gini decreases from 0.790 to 0.759 and top-10% share from 0.588 to 0.531; on ProofNet, the corresponding changes are 0.505 to 0.443 and 0.241 to 0.229. Bootstrap intervals over problems show that the Gini reductions are stable for the matched hybrid comparison (+0.031 [0.010, 0.055] on CombiBench; +0.062 [0.035, 0.090] on ProofNet), while top-10% reductions have the same sign but wider intervals (Appendix 8.1). [fig:uniformity-filtered,fig:uniformity-gini] show the same pattern at the problem level and across budgets.

5.2 Downstream Proof Utility↩︎

5.2.0.1 Prover protocol.

Goedel-Prover-V2-32B receives up to 64 deduplicated candidates per problem from the \(T=100\) semantically accepted repertoire; empty repertoires count as failures. The single-reference GT control uses the dataset reference statement. Table 2 reports solved-problem counts for pass@64, complete@64, and theorem-complete@64. The prover sees only candidates with compile_ok\(=1\) and semantic_ok\(=1\), deduplicated under canonicalization and capped at 64 statements per problem. The GT reference row runs the same prover on the dataset-provided formal statement and bypasses both generator and semantic judge.

5pt

5.2.0.2 Theorem-complete gains and boundaries.

On CombiBench, FormalEvolve raises theorem-complete@64 from 9/100 for the matched hybrid no-archive control to 13/100, and from 8/100 for both Sample and Kimina Compile+Semantic Repair. On ProofNet, FormalEvolve also improves over the matched hybrid control on theorem-complete@64 (45/186 vs./186), while remaining comparable to Kimina Compile+Semantic Repair (45/186 vs./186). Paired bootstrap intervals for the matched-hybrid theorem-complete deltas are above zero (+0.040 [0.033, 0.110] on CombiBench; +0.027 [0.021, 0.043] on ProofNet; Appendix 8.1), supporting the hedging motivation: diverse repertoires increase the chance of reaching a prover-friendly accepted statement under a fixed prover budget. Appendix 7.2 and Appendix 9.2 provide additional curves and audit details.

5.3 Stronger-Base and Manual Audits↩︎

Stronger-base statement-generation. As a supplementary CombiBench statement-generation check, we use Goedel-Formalizer-V2-8B seeding and GPT-5.4 repair with the same judge and \(T{=}100\) accounting. FormalEvolve preserves the pattern over the matched hybrid control: SH@100 rises from 0.86 to 0.88, deduplicated SemOK\(_\text{total}\) rises from 1886 to 3238 (1.7\(\times\)), and concentration drops in both Gini (0.4832 to 0.4383) and top-10% share (0.3128 to 0.2202) (Appendix 8.3).

Manual faithfulness calibration. Manual audits calibrate selected statement-stage and theorem-complete slices. On a matched 50-problem ProofNet statement-stage audit, FormalEvolve, Hybrid control, and Sample have similar Faithful/Partial/Severe totals: 42/5/3, 43/4/3, and 43/3/4. In this slice, archive search does not visibly amplify judge-positive semantic shift relative to the no-archive controls. At the theorem-complete end, a 161-artifact audit over the original three-method pool shows that FormalEvolve yields the largest absolute count of faithful artifacts (41), while severe counts are numerically similar across methods (11, 10, and 12). Proof success certifies the encoded formal statement, but not its faithfulness to the source statement; we therefore report proof success together with semantic faithfulness auditing (Appendix 9.1).

6 Conclusion↩︎

FormalEvolve is a compile-gated test-time search method for Lean 4 autoformalization under a fixed generator-call budget. The central lesson is that autoformalization should be evaluated at the level of budgeted, semantically filtered repertoires: faithful variants of the same informal claim can expose different prover-facing interfaces. FormalEvolve operationalizes this view with a compilation-feasible archive that stores reusable candidates, expands them through repair and evolution, and filters the resulting repertoire for downstream proving. Across two benchmarks, this archive-based organization improves semantic coverage, reduces cross-problem concentration, and yields theorem-complete gains over matched no-archive multi-candidate controls under our fixed prover protocol. The same archive-and-filter pattern may also extend to Coq, Isabelle, and related proof assistants, where multiple faithful formalizations can likewise differ in downstream prover utility.

Limitations↩︎

Semantic consistency remains difficult to certify automatically, which is a central challenge for autoformalization. Our semantic metrics rely on an LLM-as-judge implementation of \(\mathsf{Sem}\), so results that use semantic labels–including semantic coverage, semantic-success counts, and concentration statistics–can depend on the judge model, prompt, and serving details. Compilation certifies Lean elaboration and type correctness, while semantic equivalence to the informal problem remains outside the compiler’s guarantee. We therefore report manual faithfulness audits over outputs produced by our pipeline. On the matched ProofNet statement-stage slice, FormalEvolve, Hybrid control, and Sample have similar Faithful/Partial/Severe totals (42/5/3, 43/4/3, and 43/3/4), suggesting that archive search does not visibly amplify judge-positive semantic shift relative to no-archive controls.

Proof utility also depends on the chosen prover, proof budget, and prompting details. Our pass@64, complete@64, and theorem-complete@64 results use one fixed prover configuration with \(B=64\) attempts, so they measure utility under this protocol; broader gains across other provers and proof-search policies require separate evaluation.

7 Additional Results↩︎

We give the metric definitions used throughout the experiments, followed by statement-level decompositions, proof-utility decomposition, and budget-sweep coverage gaps under the same generator-call accounting.

7.1 Metric definitions↩︎

We provide definitions of all reporting metrics under generator-call accounting. For a given problem, let \(E_t\) denote the set of candidates evaluated up to debited call \(t\), and let \(E_t^{\mathrm{feas}}=\{c\in E_t : \mathsf{Comp}(c)=1\}\). Let \(G_t=\{c\in E_t : \mathsf{Comp}(c)=1 \wedge \mathsf{Sem}(c)=1\}\), and for dataset-level concentration let \(s_j(t)\) be the number of semantic-success candidates for problem \(j\) at budget \(t\). For proof utility, let \(S_t^{(64)}\) denote the first 64 statements in \(\tilde{G}_t=\mathrm{Dedup}(G_t)\) used by the fixed prover protocol. Let \(P_{\mathrm{pass}}(c)\in\{0,1\}\) indicate whether the prover returns a Lean 4-accepted proof script for \(c\) (warnings allowed; sorry permitted), \(P_{\mathrm{complete}}(c)\in\{0,1\}\) indicate a complete proof without sorry, and \(P_{\mathrm{theorem}}(c)\in\{0,1\}\) indicate a complete proof of an explicit theorem/lemma.

2pt

7.2 Proof utility decomposition↩︎

Figure 5 decomposes theorem-complete@64 into (i) whether a method produces a non-empty statement repertoire to attempt under the fixed prover protocol, and (ii) whether at least one attempted statement is solved at theorem-complete level under the same attempt budget.

None

7.3 Statement-level decompositions at \(T=100\)↩︎

Tables 4 and 5 decompose the fixed-budget statement-level results. FY is compilation yield, SD is semantic density conditional on compilation, and SY is semantic yield per generator call (treating compilation failures as semantic failures). Reporting FY/SH/SD/SY together separates gains from (i) producing more compilable candidates, (ii) improving semantic consistency among compilable candidates, and (iii) reallocating budget between proposal and repair.

7.4 Coverage gaps across the budget↩︎

Figure 6 reports the budget-sweep coverage gap relative to the strongest Kimina sampling baseline. The hybrid Kimina+Qwen3 baseline in Table 1 separates search effects from patch-model strength under the same generator-call accounting and repair protocol as the sampling baselines.

None

8 Analysis↩︎

We provide additional measurements for the fixed-budget experiments: paired uncertainty, repair-call composition, prover-stage non-dominance, cross-problem concentration, stronger-base behavior, and component effects.

8.1 Paired uncertainty, call composition, and prover non-dominance↩︎

The measurements below are computed from the same fixed-budget artifacts used for the main figures and tables; no additional training or model runs are introduced. They cover paired uncertainty (Table 6), concentration uncertainty for the matched hybrid comparison (Table 7), per-problem repair-call composition (Table 8), and prover-stage non-dominance (Table 9).

3pt

We use paired bootstrap 95% confidence intervals for the mean difference (FormalEvolve \(-\) baseline).

3pt

We compute the intervals by resampling benchmark problems with replacement and recomputing each concentration metric on the resampled per-problem semantic-success counts.

3pt

3pt

8.2 Cross-problem uniformity: coverage and concentration↩︎

We assess whether semantic successes concentrate on a small subset of easy problems under a fixed call budget. At \(T=100\), we summarize the per-problem semantic_ok count distribution using coverage (SH@100) and concentration (Gini and top-10% share; Table 1). Figure 7 provides a compact per-problem view. For readability, we filter to problems where at least one method attains a positive semantic_ok count (otherwise the column is identically zero). We order columns by the strongest Kimina sampling baseline (Compile+Semantic Repair) using its per-problem semantic_ok counts at \(T=100\), defining an x-axis independent of ours; Figure 8 uses the same ordering for the delta visualization. This subsection uses Compile+Semantic Repair only as a fixed ordering and visualization baseline; the matched Hybrid comparisons are reported separately in Table 6 and in the main results.

8.2.0.1 Aggregate pattern under baseline ordering.

Under this baseline ordering, gains concentrate in the baseline-ranked tail: on the filtered set, \(\Delta>0\) dominates in the tail segment, while the head segment can favor the baseline (especially on ProofNet). We define head/mid/tail by splitting the baseline-ordered problems into three contiguous segments as evenly as possible within each benchmark. The table below counts how often \(\Delta=\#\texttt{semantic\_ok}(\mathrm{\small FormalEvolve})-\#\texttt{semantic\_ok}(\mathrm{\small Compile+Semantic Repair})\) is positive/negative/zero within each segment (reported as \(+/-/0\)).

None

8.2.1 Representative early semantic hits and baseline-miss instances↩︎

On each benchmark, there are 16 instances where Compile+Semantic Repair has zero semantic_ok at \(T{=}100\) while FormalEvolve attains a positive semantic_ok count. Conversely, there are 4 such instances where the baseline hits but FormalEvolve misses on CombiBench, and 3 on ProofNet. To ground the aggregate patterns above and illustrate non-dominance, Table 10 lists representative instances in both directions: where FormalEvolve reaches a semantically consistent compilable statement substantially earlier than the baseline (or the baseline has no hit within \(T=100\) calls), and where the baseline hits but FormalEvolve misses within the same call budget. These examples are computed from the debited-call logs under the same budget.

3pt

None

Across both benchmarks, FormalEvolve improves coverage and reduces concentration (see Table 1 and Figures 7–9).

None

8.3 Stronger-base statement-generation evaluation on CombiBench↩︎

8.3.0.1 Setup.

The primary comparison uses a Kimina-based stack to keep the core comparison controlled under the same generator-call budget. To test whether the search layer still helps once the base stack is substantially stronger, we run a statement-generation evaluation on CombiBench under the same \(T{=}100\) accounting with Goedel-Formalizer-V2-8B as the seeder and GPT-5.4 as the repair model. We keep the semantic judge and statement-stage reporting protocol unchanged.

8.3.0.2 Compared methods.

Sample uses Goedel-Formalizer-V2-8B alone, without repair or archive search. Compile+Semantic Repair keeps the same stronger seeder and applies bounded compile / semantic repair without an archive. Hybrid control (no archive) keeps the same stronger seeder and stronger repair stack, with archive-based search disabled. FormalEvolve then adds archive-based search on top of this no-archive control.

3pt

8.3.0.3 Interpretation.

The stronger-base statement-generation setting preserves the main qualitative pattern. Relative to the matched no-archive hybrid control, archive-based search still improves SH@100 (0.86 \(\rightarrow\) 0.88), increases deduplicated SemOK\(_\text{total}\) by 1.7\(\times\) (1886 \(\rightarrow\) 3238), and further reduces concentration (Gini 0.4832 \(\rightarrow\) 0.4383; Top-10% share 0.3128 \(\rightarrow\) 0.2202). The search layer both expands the total pool of judge-accepted candidates and makes that pool less concentrated.

8.4 What drives gains: repair versus online diversity↩︎

Under fixed budgets, bounded patch/repair calls are the dominant contributor to semantic hit rate: removing patch repair reduces SH@100 by 11/100 (CombiBench) and 13/186 (ProofNet) (Table 1). EvolAST-style fallback has a smaller and non-monotonic effect: relative to the no-EvolAST ablation, the run with EvolAST gains semantic hits on 11 CombiBench problems and loses them on 3, while on ProofNet it gains 1 and loses 5. Because semantic_ok is assigned by the LLM-as-judge implementation of \(\mathsf{Sem}\), these differences should be read as changes in the distribution of judge-accepted candidates rather than guaranteed semantic improvements.

8.4.0.1 Illustrative instances (EvolAST can help or hurt).

The examples below show one instance where EvolAST enables a semantic hit and one where it suppresses a hit under the same \(T{=}100\) budget.

8.5 Failure modes↩︎

We log (i) compilation failures, (ii) semantic drift (judge rejects), and (iii) judge/prover disagreements for qualitative inspection. The qualitative cases in Appendix 10 show representative instances of these disagreements.

8.5.0.1 Example (judge/prover mismatch).

In Appendix 10.1.3 (ProofNet 0004_exercise_6_4_2), both baselines obtain theorem-complete prover outputs under the same RR64 budget, while our best judge-accepted statement is only pass-level. This illustrates non-dominance between semantic judging and prover utility: semantic acceptance and proof success provide different evidence under fixed-budget evaluation.

9 Human and Prover-Stage Audits↩︎

9.1 Manual faithfulness audits↩︎

9.1.0.1 Audit overview.

We report two complementary manual audits with the same Faithful / Partial / Severe label set. The first audit targets theorem-complete artifacts from the three original generator-based methods at the solved end of the pipeline. The second targets the main statement-stage setting with a matched ProofNet audit over FormalEvolve, the hybrid no-archive control, and Sample.

9.1.0.2 Theorem-complete audit: scope and audit unit.

We audit the theorem-complete end of the original three-method comparison pool. The pool contains 161 theorem-complete artifacts across Sample, Compile+Semantic Repair, and FormalEvolve: 29 from CombiBench and 132 from ProofNet. The audit unit is one solved benchmark \(\times\) method \(\times\) problem cell. If a solved cell contains multiple theorem-complete attempts, we take the first theorem-complete attempt in per_problem.json order and trace it back to the corresponding source statement in rr64_dataset.jsonl.

9.1.0.3 Labels.

Faithful means that the proved formal statement matches the mathematical content of the informal target. Partial denotes a materially narrowed, incomplete, or otherwise only partially aligned statement. Severe denotes wrong-object, vacuous, or structurally broken cases that do not preserve the intended mathematical claim.

9.1.0.4 Multi-reader cross-check.

On a multi-reader cross-check subset drawn from the manually audited portion, the initial agreement rate on the Faithful / Partial / Severe labels is 92% before adjudication. Disagreements were rechecked jointly, and uncertain cases were resolved conservatively.

9.1.0.5 Aggregate pattern.

Within this audited theorem-complete pool, FormalEvolve yields the largest absolute count of Faithful artifacts (41), while Severe counts are numerically similar across methods (11, 10, and 12). Proof success certifies the formal statement that was actually encoded and proved, but does not by itself establish faithfulness to the source statement; all three audited methods still contain severe mismatches at the solved end of the pipeline. The audit therefore complements the main fixed-budget results with a direct theorem-faithfulness view at the solved end of the pipeline.

9.1.0.6 Matched statement-stage audit.

Because the statement-stage semantic metrics rely on judge-positive outputs, we also audit matched judge-positive statement-stage outputs on ProofNet. We sample 50 problems for which FormalEvolve, the hybrid no-archive control, and Sample each have a late-window compile+semantic judge-positive witness. For each method and sampled problem, the audit unit is the latest deduplicated judge-positive candidate with insertion rank in \([20,100]\). This design compares faithfulness profiles on a shared judge-positive slice; coverage is reported separately by SH@100.

9.1.0.7 Interpretation.

Under final adjudication, the matched statement-stage audit shows similar faithfulness profiles across the three methods: FormalEvolve has 42/50 Faithful candidates, Hybrid control has 43/50, and Sample has 43/50. Severe counts are also close (3/50, 3/50, and 4/50 respectively). In this slice, FormalEvolve’s judge-positive outputs have a faithfulness profile similar to the two no-archive controls, with no obvious additional semantic shift from archive search.

9.2 Prover-stage audit: what proof success certifies↩︎

9.2.0.1 Scope and claim boundary.

We audit the prover stage on the subset of judge-accepted statements produced within the generator-call budget ([sec:budget]). A prover-complete Lean file certifies that the produced formal artifact is accepted by Lean and contains no remaining sorry. Faithfulness to the original informal statement is assessed by the LLM-as-judge implementation of \(\mathsf{Sem}\) and checked with manual audits (Appendix 9.1).

9.2.0.2 Prompt reference.

The prover prompt template is fixed (Appendix [sec:appendix-prover-prompt]); the case studies report the proved formal statement and the prover response.

9.2.0.3 ASCII normalization.

For compatibility with pdfLaTeX, raw transcripts in PromptBox are displayed after ASCII-only normalization of common Unicode math symbols (e.g., rendering quantifiers and connectives in ASCII form). This affects presentation only.

9.2.0.4 Theorem-complete reporting.

In addition to standard pass@64 and complete@64, we report theorem-complete@64: a problem counts as theorem-complete@64 if at least one prover attempt yields a Lean-accepted, sorry-free file that contains an explicit theorem or lemma. This guards against Lean-complete outputs that only introduce auxiliary def/abbrev/example content without proving a named proposition.

9.2.0.5 Prompt categories.

Table 12 also reports a coarse prompt-type audit for the audited generator-based methods over prover attempts (not over problems): the denominator is the number of prover prompts actually issued under a fixed per-problem attempt budget. We label an attempt as “Prompt has theorem” if the candidate statement sent to the prover contains an explicit theorem/lemma declaration. We label an attempt as “Prompt abbrev-only” if the candidate contains an abbrev declaration and no theorem/lemma. Remaining attempts typically correspond to def or example templates and are omitted from this summary.

9.2.0.6 Takeaway.

On ProofNet, most prover prompts contain a theorem/lemma (around 0.96), so theorem-complete filtering is close to the standard metrics. On CombiBench, 9–13% of prompts are abbrev-only; theorem-complete@64 is therefore a stricter and more robust success signal.

None

None

None

10 Case Studies and EvolAST Ablation↩︎

We give representative statement/prover interactions and an EvolAST ablation to illustrate where archive search helps, where it is non-dominant, and how symbolic rewrites can change search trajectories under a fixed budget.

10.1 Case studies: two successes and one non-dominance example↩︎

10.1.0.1 Scope.

We include two short success cases that illustrate prover-stage outcomes under the same RR64 budget (one where baselines fail to produce any Lean 4-accepted proof output, and one where a baseline reaches only pass-level artifacts), plus one counterexample that highlights non-dominance and judge/prover mismatch. To contextualize these examples, Table 9 quantifies prover-stage non-dominance frequency at theorem-complete@64 (FormalEvolve versus Compile+Semantic Repair) under the same RR64 protocol.

10.1.1 Theorem-complete proof: ours completes; baselines have no pass↩︎

Benchmark: proofnet.
Problem id: 0088_exercise_4_3_1.
Informal statement:

If \(R\) is a commutative ring and \(a \in R\), let \(L(a) = \{x \in R \mid x a = 0\}\). Prove that \(L(a)\) is an ideal of \(R\).

10.1.1.1 Outcome under the same fixed \(B=64\) prover budget.

Our run attains a theorem-complete proof, while both sampling baselines fail to produce any Lean 4-accepted proof output within \(B=64\) attempts (no pass).

10.1.1.2 Takeaway.

This instance illustrates a practical benefit of a repertoire: under a fixed prover attempt budget, the ability to try multiple judge-accepted statements can be the difference between reaching a complete proof and having no Lean-accepted proof output at all.

10.1.1.3 Notation.

Lean 4 admits both Unicode and ASCII forms. For pdfLaTeX compatibility, we display prover transcripts in ASCII, where quantifiers/connectives may appear as forall/-> and the constructor names And/Or, corresponding to \(\forall/\to\) and \(\wedge/\vee\).

10.1.1.4 Abridged prover output excerpt (ours; theorem-complete).

10.1.2 Complete proof: ours completes; baseline is pass-only↩︎

Benchmark: proofnet.
Problem id: 0000_exercise_2_3_2.
Informal statement:

Prove that the products \(a b\) and \(b a\) are conjugate elements in a group.

10.1.2.1 Outcome under the same fixed \(B=64\) prover budget.

Our run reaches a theorem-complete proof (complete=True, sorries=0), while Compile+Semantic Repair only reaches pass-level artifacts with remaining sorry.

10.1.2.2 Prover output excerpt (ours; theorem-complete).

10.1.2.3 Statement evolution trace (mechanism note).

This instance illustrates why we separate compilation from semantic checking: an early candidate may compile yet express a non-standard (and generally stronger) variant of the target claim, which can be judged inconsistent and/or harder for the prover to use under a fixed attempt budget. Here, the parent uses a conjunction of two equations, whereas the informal goal is a single conjugacy statement of the form \(a*b = g*(b*a)*g^{-1}\). Bounded semantic repair removes the extra conjunct and rewrites the statement into this standard form while preserving compilation feasibility (Figure 13).

None

10.1.3 Non-dominance case: baseline theorem-complete; ours pass-only↩︎

Benchmark: proofnet.
Problem id: 0004_exercise_6_4_2.
Informal statement:

Prove that no group of order p q, where p and q are prime, is simple.

10.1.3.1 Outcomes under the same fixed \(B=64\) prover budget.

In this instance, our best judge-accepted statement yields pass=True but not a complete proof, while both sampling baselines obtain a theorem-complete proof within the same prover attempt budget.

10.1.3.2 Takeaway.

This example highlights non-dominance: even under the same prover budget, different judge-accepted statements can differ substantially in proof-search friendliness, so proof utility and semantic faithfulness need separate readouts.

10.1.3.3 Prover output excerpt (ours; pass-only).

The excerpt below contains remaining sorry; the baseline theorem-complete outputs serve as the comparison point through the reported outcome flags. Ours (pass-only):

10.2 Early proof successes under fixed prover budgets↩︎

Table 13 lists representative instances where FormalEvolve reaches a successful proof substantially earlier than Compile+Semantic Repair under the same prover attempt budget, or succeeds when the baseline fails within \(B=64\) attempts. We report the first prover attempt index \(k\) (under the round-robin schedule described in 7.1) where the prover returns (i) any proof script accepted by Lean 4 (pass) or (ii) a complete proof without sorry (complete).

2pt

10.3 Ablation note: when EvolAST changes outcomes on ProofNet↩︎

On ProofNet, enabling EvolAST slightly decreases semantic hit@100 under fixed-budget accounting (158/186 vs 162/186). The gap is small (4 problems), but it illustrates an important point for budgeted search: a diversity operator can change the search trajectory and archive composition, and may not be universally beneficial across datasets.

10.3.0.1 Where the difference comes from.

Under fixed-budget accounting, there are 5 problems that achieve at least one judge-accepted statement under the no-EvolAST configuration but not under the main configuration, and 1 problem where the reverse holds. Because the generator and patching process are stochastic, these disagreements reflect diverging search trajectories under nearly identical protocols; attributing causality to any single operator requires careful per-instance inspection. Empirically, these disagreements are consistent with a mixture of direct trigger effects (duplicates/compile-fail fallbacks), indirect trajectory effects, and dataset-dependent operator behavior.

2pt

10.3.0.2 Representative example (problem 0142_exercise_4_15a).

In this instance, the main configuration produced many compilable candidates but no semantic success, whereas the no-EvolAST configuration eventually reaches a judge-accepted statement after semantic repair. One characteristic we observe in the main run is that EvolAST fallback triggers repeatedly on duplicates and compile failures, producing compilable but judge-rejected variants; in this problem, many candidates are explicitly tagged as EvolAST fallbacks, and all have \(\mathsf{Comp}(c)=1\) but \(\mathsf{Sem}(c)=0\). This can bias the archive toward structurally perturbed but semantically misaligned candidates under a fixed budget, which in turn alters parent selection and patch contexts.

Concretely, the semantic judge flags a common failure mode here: domain mismatch (e.g., proving uniform continuity on \(\mathbb{R}\) with the intended \([a,b]\) restriction missing). The best candidate found by the main run (compilable but judge-rejected) has the unconstrained target:

whereas the successful no-EvolAST semantic-repair output explicitly restricts the bound to \(s,t\in [a,b]\) and targets uniform continuity on the interval:

This illustrates a fundamental limitation of a conservative type-rewrite operator: our EvolAST rule set is limited to the existing binder and goal AST, so new problem-specific binders (e.g., explicit \(a,b\) interval parameters) and new domain-restriction hypotheses require LLM repair. Therefore, when the current parent trajectory has not yet reached a semantically correct “skeleton”, applying EvolAST tends to preserve the same semantic mistake, producing many feasible variants that remain judge-rejected. This effect is amplified by our implementation choice that EvolAST candidates terminate the fallback path to keep accounting bounded, leaving later semantic correction to subsequent LLM proposals.

10.3.0.3 Takeaway.

Online diversity operators can have dataset-dependent effects on semantic hit rates under a fixed budget. In practice, this motivates tunable EvolAST rule sets, tunable trigger conditions, and transparent ablation reporting.

10.3.0.4 EvolAST rewrite surface.

In our experiments, EvolAST is used in its rule-based mode: it applies a bounded sequence of conservative, semantics-intended AST rewrites to the theorem type (binder types and goal type), keeping the proof body unchanged. The rewrite surface is intentionally controlled and includes conservative hypothesis reordering; commutativity/associativity/distributivity for conjunction/disjunction (Lean: \(\wedge/\vee\)); symmetry swaps (e.g., \(a=b\) to \(b=a\), \(P\leftrightarrow Q\) to \(Q\leftrightarrow P\)); and dual relations (e.g., \(a<b\) to \(b>a\), \(a\le b\) to \(b\ge a\)).

11 Algorithm, Budget Accounting, and Configuration↩︎

We give the detailed per-problem search procedure, generator-call accounting rules, semantic-judge overhead, and implementation configuration used in the fixed-budget experiments.

11.1 Detailed Pseudocode↩︎

11.1.0.1 Accounting conventions.

Under fixed-budget accounting, we debit only generator-side LLM calls (proposals and bounded repairs). EvolAST is a symbolic fallback triggered on (i) exact duplicates after canonicalization and (ii) compilation failures; it does not consume generator-call budget and is evaluated as the representative candidate of the triggering call. Each compilation-repair or semantic-repair attempt is itself a debited generator call whose representative candidate is the repaired output; semantic repair preserves the original compilable candidate and appends a repaired variant, and both are evaluated. All metrics normalize by the fixed budget \(T\) per problem; any early termination or failed call is treated as a consumed call with \(\mathsf{Comp}(c)=0\) and \(\mathsf{Sem}(c)=0\).

11.1.0.2 Parent selection.

Parent selection uses the usage-penalized robust weighting described in Section 3. For completeness, each archived candidate \(c_i\) has gate score \(s_i=\mathsf{Comp}(c_i)(1+\mathsf{Sem}(c_i))\) and parent-usage count \(n_i\). Within the selected island, we set \(z_i=(s_i-m)/d\), where \(m=\mathrm{median}_j(s_j)\) and \(d=\max(\mathrm{MAD}(\{s_j\}_j),10^{-6})\). The quality factor is \(Q_i=\sigma(\lambda z_i)\), the reuse factor is \(R_i=[1+(1+\beta)n_i]^{-1}\), and the next parent is sampled with probability \(Q_iR_i/\sum_j Q_jR_j\). Here \(\mathrm{MAD}(A)=\mathrm{median}_{a\in A}|a-\mathrm{median}(A)|\), \(10^{-6}\) is a numerical stabilizer, and \(R_i\) discourages repeatedly selecting the same parent.

11.2 Budget Audit and Evaluation Overhead↩︎

11.2.0.1 Generator-side.

We audit generator-call usage under the budget currency (\(T=100\) calls per problem). We decompose the fixed budget \(N\times T\) into generation calls (Gen), compilation-repair calls (CRep), and semantic-repair calls (SRep). Table 8 provides a complementary per-problem distributional view (median/IQR) of CRep/SRep under the same accounting.

11.2.0.2 Evaluator-side (semantic judge).

We report evaluator overhead in terms of semantic LLM-as-judge calls (CriticLean-Qwen3-14B). In this pipeline, semantic judging is invoked only after successful compilation, and EvolAST outputs are judged under the same gate; EvolAST-Judge is the subset of judge calls attributed to EvolAST-labeled candidates (generator-call-free on the generator side).

4pt

4pt

11.3 Configuration and hyperparameters↩︎

Table 17 summarizes the key hyperparameters used in the main experiments.

11.3.0.1 Lean 4 toolchain and library.

All candidates are compiled under Lean 4.15.0 with Mathlib (import Mathlib). We use Mathlib4 v4.15.0 (commit 9837ca9) as bundled by our Kimina Lean Server installation. Compilation is served by Kimina Lean Server [22], which provides a pinned Lean 4/Mathlib environment suitable for large-scale batch checking.

11.3.0.2 Implementation notes: archive and island mechanics.

• Global feasible archive. We maintain a global compilation-feasible archive (capacity 40); selection is applied only within this feasible set.

• Island-local behavior. Parent selection and cross-patch inspirations are restricted to the sampled island (via island_idx); children inherit the parent island by default.

• Migration. Every 10 generations, we migrate a small fraction of feasible candidates between islands (rate 0.1), while protecting the top-1 elite in each island.

12 Prompting and Semantic-Judge Protocol↩︎

We report the prompt templates used for initial statement generation, evolution operators, bounded repair, semantic judging, and downstream proof completion. We show the full prompt skeletons because prompt details affect both reproducibility and the reliability of LLM-as-judge semantic labels.

12.0.0.1 Notation.

Placeholders include {informal} (natural-language statement), {code_content} (current Lean file), {performance_metrics} (compile/semantic metrics), {text_feedback_section} (optional judge feedback), {original_code} (candidate file for repair), {compile_error_type}/{compile_error_msg} (compiler feedback), {critic_feedback} (semantic-judge feedback), {inspiration_code_1} (cross inspiration), and {lean_statement} (theorem statement for judging). For pdfLaTeX compatibility, we render common Lean unicode symbols in ASCII in verbatim displays.

12.1 Statement generation (initial)↩︎

12.1.0.1 Prompt template.

12.2 Evolution operators (full / diff / cross)↩︎

12.2.0.1 Shared prompt skeleton.

12.2.0.2 Full-mode addenda (sampled variants; one per call).

Diff mode prepends a short local-edit instruction (still returning a full file), while cross mode additionally provides one sampled inspiration candidate from the archive/top-k pool as extra context.

12.2.0.3 Diff-mode prefix (local edit).

12.2.0.4 Cross-mode prefix (inspiration-guided).

12.2.0.5 Cross-mode extra context (one per call).

12.3 Bounded repair prompts↩︎

Repairs count toward the generator-call budget. Compilation repair triggers only when compile_ok=0; semantic repair triggers only when compile_ok=1 and semantic_ok=0.

12.3.0.1 Compilation repair prompt.

12.3.0.2 Semantic repair prompt.

12.4 Semantic judge prompt (CriticLean-Qwen3-14B)↩︎

We use CriticLean-Qwen3-14B as the LLM-as-judge implementation of \(\mathsf{Sem}\), judging semantic consistency between the natural-language statement and the Lean 4 theorem statement (proof ignored). The prompt template below is used for each semantic check.

12.5 Prover prompt (Goedel-Prover-V2-32B)↩︎

We evaluate downstream proof utility using a fixed prover configuration (Goedel-Prover-V2-32B) and a fixed prompt template. The prompt asks the prover to complete a Lean file by replacing the placeholder proof.

References↩︎

---

1. Corresponding author: wangwei@nlpr.ia.ac.cn.↩︎