PaperlayerView exact revision on arXiv

Source-linked AI summary

AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness

Prithwish Jana, Viet Bach Hoang, Logan Luna, Viresh Pati, Akash Singirikonda, Cy Xie, Lisa Carbone, Wuyang Chen, Walter Moreira, Joe Stubbs, Sriram Vishwanath, Vijay Ganesh

arXiv:2610.05367v1cs.LOcs.AIcs.LG

TL;DR

Research-level proof auto-formalization faces costly, complex proofs and limitations in training data and harness design. AIProver jointly post-trains an open-weight model and evolves its harness with verifier feedback; it improves pass@4 semantic correctness over its Leanstral-1.5 base and as a skill for Claude Code and Codex.

  • Problem

    Research-level proof auto-formalization must handle long chains of interdependent definitions and proofs, while affordable autonomous approaches and research-level training data remain limited.

    Source: §1 · pp. 1–2

  • Method

    AIProver jointly post-trains an open-weight LLM and evolves its harness using verifier rewards and certificates for completeness, type correctness, and semantic correctness.

    Source: §1 · p. 2, §4.2.2 · p. 6

  • Results

    36.7% pass@4 semantic correctness, up from 15.7% for Leanstral-1.5, beats OpenGauss (21.5%) and Aristotle (18.4%).

    Source: §1 · p. 3

  • Takeaways & Limitations

    As a skill, AIProver raises Claude Code semantic correctness from 41.9% to 79.8% and Codex from 34.1% to 62.4%.

    Source: §5.3 · p. 9

    No reliable check for NL–FL proof faithfulness exists; heuristic LLM judges are stochastic and slow when scoring many rollouts concurrently.

    Source: §4.2.1 · p. 5

Abstract

from arXiv · show

Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, research-level proofs often depend on concepts missing from leading proof assistant libraries (e.g., Lean's Mathlib), and successful compilation does not guarantee that a translation preserves the theorem's meaning or the proof's reasoning. Furthermore, aligned NL-FL training data are scarce, and leading agents often rely on costly frontier models and manually engineered harnesses. To address the above issues, we present AIProver, an agentic framework for autonomous proof auto-formalization and proof synthesis (AFPS) that jointly post-trains a 119B open-weight language model and evolves its agentic, tool-calling harness with HarnessEvolve. Verifiers assess type correctness, proof completeness, and semantic correctness, returning rewards and diagnostic certificates that drive model fine-tuning and alternating reinforcement learning via symbolic feedback and HarnessEvolve, a certificate-driven evolutionary search over the whole harness control flow that re-tailors the harness to the updated model. For research-level training and evaluation, we introduce LoCoBench, 58.9k instances from Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook, with a 771-instance validation split whose theorem-proof pairs have no public Lean formalization. Against 39 frameworks spanning AFPS agents, frontier LLMs, and coding agents, AIProver lifts pass@4 semantic correctness over its Leanstral-1.5 base from 15.7% to 36.7% and outperforms every other open-weight system and Aristotle. As a Claude Code and Codex skill, it lifts their semantic correctness from 41.9% and 34.1% to 79.8% and 62.4%, respectively. Further, it is also 24% cheaper than Numina-Lean-Agent, pushing the accuracy-cost frontier of research-level AFPS.

1 INTRODUCTION

Research-level proof auto-formalization faces semantic, data, cost, and harness-design challenges. AIProver jointly trains an open-weight model and evolves its harness, improving semantic correctness on LoCoBench and when paired with coding agents.

1 INTRODUCTION

  • Research-level proofs involve long chains of interdependent definitions and lemmas, while compiled Lean code can still prove the wrong theorem or silently repair flawed NL reasoning.Prior agents also face cost, human-in-the-loop, jagged-intelligence, and accessibility limitations.Source: §1 · pp. 1–2
  • AIProver targets autonomous, affordable research formalization with an open-weight model, unattended operation, semantic and proof fidelity, and use as a specialist skill for frontier agents.The authors identify semantic alignment, fine-grained training signals, research-level data, and AFPS-tailored harness design as four obstacles.Source: §1 · p. 2
  • LoCoBench contains 58.9k instances, including a 771-instance validation split without public Lean formalizations to retrieve or imitate.The benchmark draws on Mathlib, CSLib, Mizar, and a bounded-arithmetic textbook.Source: §1 · p. 2
  • AIProver alternates harness evolution with model post-training, using verifier rewards and certificates for completeness, type correctness, and semantic correctness.The stated contribution is an agent that post-trains an open-weight LLM while evolving its harness.Source: §1 · p. 2
  • 36.7% pass@4 semantic correctness, up from 15.7% for Leanstral-1.5, beats OpenGauss (21.5%) and Aristotle (18.4%).With Claude Code, AIProver reaches 79.8% versus 41.9% for Claude Code alone; with Codex, it reaches 62.4% versus 34.1% for Codex alone.Source: §1 · p. 3

2 RELATED WORK

Prior auto-formalization systems either chain separate formalization and proof models or use end-to-end verification, but none of the described approaches combines research-level agentic AFPS with the paper’s joint model-and-harness optimization. AIProver makes semantic alignment part of training and harness selection.

2 RELATED WORK

  • Chained formalization and proof-synthesis models can cascade errors and do not verify or correct each other; cited end-to-end systems use small models or closed APIs and lack research-level agentic evaluation.The passage names Draft, Sketch, and Prove, ProofFlow, ToMap, and ProofBridge among end-to-end approaches.Source: §2 · p. 3
  • AIPROVER post-trains a 119B open-weight LLM on rewards that verify completeness, type correctness, and semantic correctness for long-horizon research-level AFPS.This is the paper’s stated distinction from prior systems that chain separate models or use small models or closed APIs.Source: §2 · p. 3
  • Existing AFPS harnesses optimize type correctness, while automated harness search typically mutates prompts, skills, or memory rather than control flow.AIPROVER’s HarnessEvolve searches full harness control flow for semantic correctness while alternating with RL to tailor the harness and model to each other.Source: §2 · p. 3
  • AIPROVER uses semantic alignment as a training signal: SAM builds NL–FL equivalence into the model, RL rewards semantic correctness, and HarnessEvolve selects harnesses by that reward.The stated objective is to preserve meaning, not merely achieve compilation.Source: §2 · p. 3

3 PRELIMINARIES AND PROBLEM STATEMENT

The paper defines proof auto-formalization as mapping a self-contained NL theorem-and-proof passage to an equivalent Lean pair. Equivalence requires type correctness, completeness, semantic correctness, and proof faithfulness, with Lean and a judge handling different checks.

3 PRELIMINARIES AND PROBLEM STATEMENT

  • An agent pairs an LLM with a harness, the software layer governing context, tools, memory, and control flow in a stateful environment.The paper focuses on ReAct-style Python harnesses and optimizes both the model and harness.Source: §3 · p. 3
  • The input is a self-contained NL passage containing a theorem and its proof; the output is an equivalent Lean theorem-and-proof pair with definitions and auxiliary lemmas.The NL passage may include assumptions and intermediate lemmas.Source: §3 · pp. 3–4
  • The AIPROVER pipeline combines LoCoBench, NL–FL alignment, whole-control-flow harness evolution, and post-training on graded verifier reward.Each round evolves the harness for the current model, then post-trains the model in that harness.Source: Figure 1 · p. 4
  • Equivalence requires type correctness, completeness, semantic correctness, and proof faithfulness; Lean checks the first two, while a judge assesses the NL-to-FL properties.Semantic correctness preserves the theorem under the same definitions without adding assumptions or dropping conditions; proof faithfulness preserves the NL proof strategy without new assumptions.Source: Figure 2 · p. 3, §3 · p. 4

4 PROPOSED METHODOLOGY

AIProver alternates harness evolution and model post-training, retaining each paired update only when held-out fitness improves. Its methodology aligns natural-language and formal representations, uses verifier rewards and certificates, searches harness control flow, and trains multi-turn agents with symbolic feedback.

4.1 SEMANTIC ALIGNMENT MODEL (SAM) FINE-TUNING

  • SAM jointly trains a contrastive alignment objective and language modeling so the decoder represents NL theorems and proofs and their FL counterparts as the same mathematical object.The NL and FL views are constructed to align on meaning without shared context; the projection head is discarded at generation, so alignment affects generation through the shared adapters.Source: §4.1 · p. 5

4.2.1 REWARD DESIGN

  • The reward combines type correctness, completeness, semantic equivalence, and proof-length fidelity, while certificates report diagnostic results in order of the checks.No reliable NL–FL faithfulness check exists, so the reward is built around sound formal verifiers; a matched theorem outweighs completeness, and proof length can reduce a solved instance’s reward by at most 0.10.Source: §4.2.1 · pp. 5–6

4.2.2 HARNESSEVOLVE: CERTIFICATE-DRIVEN EVOLUTIONARY SEARCH

  • HarnessEvolve mutates and evaluates harnesses with the model frozen, using a search memory of accepted and rejected designs, fitness, and per-instance certificates.A coding agent uses those certificates to identify recurring failures and alter control flow; each child is evaluated across instances, and only a child exceeding the best fitness is accepted.Source: §4.2.2 · p. 6

4.2.3 AGENTIC RLSF: MULTI-TURN POST-TRAINING VIA SYMBOLIC FEEDBACK

  • Agentic RLSF post-trains the model inside a frozen harness, rewarding only the final Lean file with verifier-based outcomes and optimizing generated tokens using GRPO.Its fine-grained reward ladder distinguishes ill-typed, incomplete, and complete proofs, including within groups whose rollouts all fail under binary rewards.Source: §4.2.1 · p. 6, §4.2.3 · p. 7

5 EXPERIMENTAL EVALUATION

The evaluation introduces LoCoBench and compares AIPROVER with 39 systems using pass@4 measures of compilation, semantic correctness, and proof completeness. AIPROVER improves over its Leanstral-1.5 base, leads open-weight systems as a standalone agent, and raises accuracy when integrated with Claude Code or Codex.

5.1 LOCOBENCH: A BENCHMARK FOR RESEARCH-LEVEL MATHEMATICS

  • LoCoBench contains 58.9k research-level instances from Mathlib, CSLib, Mizar, and a bounded-arithmetic textbook, across algebraic structures, foundations, logic and complexity, and number theory.Mathlib and CSLib pairs are separated into standalone files with dependencies resolved and individually type-checked; Mizar pairs are likewise split into standalone files.Source: §5.1 · p. 7

5.2 STATE-OF-THE-ART BASELINES AND EVALUATION METRICS

  • Table 3 compares 39 systems across fields and overall using pass@4 for compilation, semantic correctness with or without sorry, and complete proofs.The table reports pass@4 percentages; bold and underlining denote the best and second-best value per column.Source: Table 3 · p. 8
  • Semantic correctness on the 771-instance validation set requires agreement from two frontier judges on both Lean-to-gold and informalized-output-to-input comparisons.The protocol does not score proof faithfulness because no reliable check is available and LLM judges are less reliable on proofs than theorems.Source: §5.2 · p. 8

5.3 EXPERIMENTAL RESULTS

  • 36.7% pass@4 TC+SC full proofs for AIPROVER exceeds OpenGauss’s 21.5% and the 34.1% of Codex; only Claude Code scores higher at 41.9%.On number theory, AIPROVER reaches 67.0%, above Codex at 62.0% and Claude Code at 57.0%.Source: §5.3 · p. 9
  • 79.8% with Claude Code and 62.4% with Codex exceed the hosts alone and prior Lean-agent integrations on semantic correctness.With Numina-Lean-Agent, Claude Code reaches 72.5% and Codex 44.5%; with OpenGauss, they reach 54.3% and 41.9%, respectively.Source: §5.3 · p. 9
  • 36.7% full proofs and 94.8% type-correctness follow interleaved RLSF and HarnessEvolve, versus Leanstral-1.5’s 12.6% and 27.4%.The seed harness raises full proofs to 15.7%; HarnessEvolve raises them to 22.6%, while SAM alone lowers them from 3.0% to 1.4%.Source: §5.3 · p. 9
  • AIPROVER’s three configurations form a cost-performance frontier, with higher accuracy and lower cost than prior harnesses when paired with either coding agent.With Claude Code, it reaches 79.8% at $1.55/attempt versus Numina-Lean-Agent’s 72.5% at $2.03; with Codex, it reaches 62.4% at $0.85 versus 44.5% at $1.08.Source: §5.3 · p. 9

6 CONCLUSION

AIProver combines open-weight model post-training with an evolving harness, using verifier feedback to improve both across rounds. On LoCoBench-Val it outperforms open-weight systems standalone and makes Claude Code and Codex more accurate and cheaper than prior harnesses.

6 CONCLUSION

  • Figure 4 characterizes AIProver as forming the accuracy-cost Pareto frontier.Source: Figure 4 · p. 9
  • AIProver alternates model post-training from verifier rewards and certificates with harness evolution, adapting the harness to the improved model each round.Verifiers assess type correctness, completeness, and semantic correctness; Agentic RLSF post-trains the model in the improved harness.Source: §6 · p. 9
  • On 771 LoCoBench-Val instances from Mizar and a textbook, AIProver beats every open-weight system standalone and makes Claude Code and Codex more accurate and cheaper than prior harnesses.The conclusion frames these results as showing that an open-weight LLM can serve as a research-level auto-formalizer when post-trained on verifier feedback and paired with an adapted harness.Source: §6 · p. 9

A.1 REPRODUCIBILITY AND IMPLEMENTATION DETAILS

The implementation combines a fixed-data HarnessEvolve search, multi-turn Agentic RLSF, and LoRA-based model training. Training and evaluation use separate hardware roles, with Lean 4.23.0 and matching Mathlib throughout.

A.1 REPRODUCIBILITY AND IMPLEMENTATION DETAILS

  • CPU-side agent loops, Lean servers, harness search, and evaluation run on a 32-core, 125-GiB VM; model hosting and training run on H100 and H200 clusters.Experiments use Lean 4.23.0, Lake 5.0.0, matching Mathlib, and Python 3.12.Source: §A.1 · p. 17
  • HarnessEvolve searches over a frozen 300-instance training set sampled from a 1,000-instance pool, with eligibility rules that limit repeated node selection and encourage exploration.Candidate harnesses must parse and run, retain the seed model settings, differ from prior nodes, and contain no gold Lean; rounds with too many unresolved verifier verdicts are invalid.Source: §A.1 · p. 17
  • Agentic RLSF trains the multi-turn agent for 20 optimization steps per round, using 32 instances and eight rollouts per instance.Advantages are centered by the group mean without standard-deviation scaling.Source: §A.1 · p. 17
  • RLSF instances come from about 16,700 LoCoBench-Train instances, disjoint from the HarnessEvolve pool and the 500-instance round-gate set.The round gate requires at least a 0.024 improvement in mean reward.Source: §A.1 · p. 18
  • The semantic alignment model uses rank-32 LoRA adapters on five latent-attention projections across 36 decoder layers, plus a two-layer projection head from 4096 to 512 dimensions.The frozen base is Leanstral-1.5-119B-A6B, with about 6B parameters active per token; the experts are untouched.Source: §A.1 · p. 18
  • Training uses AdamW with peak learning rate 10^-4, cosine decay, 3% warmup, and batches of up to 32 pairs for two epochs.SFT and SAM share the configuration, seed, and batch order, differing only in λ.Source: §A.1 · p. 18

A.2 BENCHMARK DETAILS

LoCoBench combines formalized and natural-language-only research-level theorem–proof pairs, with a validation split drawn from sources without Lean-labeled training examples. Its construction preserves standalone formal developments and tests systems on longer, harder material than prior benchmarks.

A.2.1 INSTANCES AND SOURCES

  • LoCoBench includes 18,757 Mathlib and CSLib instances with verified Lean formalizations, plus 39,385 Mizar and 71 textbook instances carrying natural language only.The textbook pairs come from a research-level bounded-arithmetic text, a topic neither library formalizes.Source: §A.2.1 · p. 18

A.2.2 EXTRACTION PER SOURCE

  • Mathlib and CSLib extraction uses dependency analysis to produce 18,757 standalone Lean files, each type-checked and containing one theorem.The extraction resolves imports and namespaces rather than copying dependencies, and failed files are discarded.Source: §A.2.2 · p. 18
  • Mizar articles are classified into mathematical domains by title rules, then split into standalone theorem files carrying their required definitions and auxiliary theorems.The selection excludes 1,810 theorems from articles that matched no domain rule.Source: §A.2.2 · p. 19

A.2.3 INFORMALIZATION

  • Natural-language theorem–proof pairs are produced by informalizing formal sources, a direction the paper describes as more reliable because formal statements make hypotheses and proof steps explicit.Formalization instead requires recovering implicit assumptions and skipped reasoning from natural language; drafts are checked by a separate semantic-intent judge and failures flagged for manual review.Source: §A.2.3 · p. 19

A.2.4 TRAIN/VAL SPLIT

  • 771 validation instances come from Mizar and bounded-arithmetic textbook sources, with no validation source appearing with Lean labels in training.The split contains 700 Mizar instances and 71 textbook instances; bounded arithmetic is absent from the training libraries.Source: §A.2.4 · p. 20
  • The 700 Mizar validation theorems are selected across articles, favoring long proofs, while the 71 textbook pairs test bounded arithmetic absent from training.The Mizar selection samples 100 theorems per domain across articles; picked proofs have median lengths of 360–685 Mizar lines, depending on domain.Source: §A.2.4 · p. 20
  • Validation is harder than Train and prior benchmarks on every reported measure, with median theorem and proof lengths of 283 and 708 words.The corresponding medians are 64 and 159 words for Mathlib Train and 22 and 91 words for ProofNet; validation is scored by type-checking and a semantic-correctness judge because it lacks gold Lean.Source: §A.2.4 · p. 20

A.2.5 GROUPING DOMAINS INTO FIELDS

  • The eight domains are reported in three fields: Algebraic Structures, Foundations, Logic & Complexity, and Number Theory.The grouping reflects proof style, and keeps the nearly half-benchmark share of Ring Theory and Group Theory from masking smaller fields.Source: §A.2.5 · p. 20

A.4 EVALUATION PROTOCOL

The evaluation combines type checking with semantic judgments because semantic correctness cannot generally be decided mechanically. It uses multiple judge views and extends equivalence checking to distinguish near-misses, while the skill protocol assigns proof search and semantic review to different agents.

A.4.1 THE SEMANTIC-CORRECTNESS JUDGE

  • The two semantic comparisons catch different errors: formal comparison can expose changed quantification, while informal comparison can expose mistranslated definitions.Textbook instances lack gold formal statements and receive only the informal-to-informal comparison.Source: §A.4.1 · pp. 21–22
  • Semantic correctness requires four independent verdicts: two judges must accept both formal-to-formal equivalence and informal-to-informal agreement.Both formal-to-formal tiers must be full or partial, and both informal-to-informal verdicts must be yes; any no rejects the candidate.Source: §A.4.1 · p. 22

A.4.2 EXTENDING BEQ+ FOR THE SEMANTIC-CORRECTNESS CHECK

  • BEq+ is extended to score one-way equivalence as a near-miss, assigning 0.5 rather than 0 when a candidate is provably weaker or stronger.The two directions are tested separately, including a swapped retry when the first direction fails; the graded score matters under group-relative RL.Source: §A.4.2 · p. 22
  • Before accepting a BEq+ match, the check rejects statements provable alone, preventing a trivial candidate from matching an easy gold theorem.A pair proved in both directions by exact? using the other statement is exempt because the proof depends on the actual counterpart.Source: §A.4.2 · p. 22

B AIPROVER AS A SKILL FOR FRONTIER CODING AGENTS

  • As a skill, AIPROVER searches for Lean proofs while the host agent judges semantic correctness and proof faithfulness, fixes statements, and composes returned pieces.AIPROVER sessions run for up to 200 turns; the host does not search for proofs itself.Source: B AIPROVER AS A SKILL FOR FRONTIER… · p. 22
  • The host protocol first builds a blueprint, then tries four full samples before decomposing failures into frozen-context proof pieces and rerunning final checks.The host accepts the first sample passing type correctness, completeness, semantic correctness, and faithfulness.Source: B AIPROVER AS A SKILL FOR FRONTIER… · p. 23

C DATA DISTILLATION

The data-distillation pipeline generates Lean proof examples, checks compilation and semantic alignment, and releases filtered Mathlib and Mizar data. Its results show distinct yield and validation challenges across the two sources, while the accompanying analysis describes how semantic alignment is tested in the model’s hidden representations.

C.2 GENERATION CONFIGURATION

  • Mathlib examples are generated with Claude Opus 5, while Mizar examples use DeepSeek-V4-Flash; both runs allow one repair attempt.Distillation attempted 18,747 Mathlib/CSLib and 39,123 Mizar instances.Source: C DATA DISTILLATION · p. 23, §C.2 · p. 25

C DATA DISTILLATION

  • The pipeline parses generated formalizations, compiles them, may return failures for repair, then filters for semantic equivalence using BEq+ or a calibrated LLM judge.Compile success and semantic quality are treated as separate quality checks.Source: C DATA DISTILLATION · p. 23
  • Mathlib distillation compiled 88.39% of attempted examples, while BEq+ found 75.5% semantically equivalent, a 12.9-point gap.The released split contains 16,570 compiled traces, each with BEq+ and judge verdicts; 12,500 are BEq+-equivalent.Source: C DATA DISTILLATION · p. 24
  • Mizar distillation compiled 24.1% of attempts and yielded a 12.4% upper bound on semantically correct examples because no gold Lean statements were available.The released Mizar split has 6,799 instances that compile, carry a chain-of-thought, and pass the training-pair validator.Source: C DATA DISTILLATION · p. 24

C.3 REPAIR

  • Repair replaces an original generation only when it improves the verification outcome.The repair prompt strips few-shot examples that account for roughly 70% of prompt tokens.Source: §C.3 · pp. 25–26

D COST ACCOUNTING

  • Each reported cost combines frontier-agent tokens and local-model GPU time; AIPROVER’s local GPU allocation is valued at $0.32 per attempt.Numina Lean Agent’s greater expense is associated with a 15-turn loop per attempt versus 1.8 turns for Claude Code.Source: D COST ACCOUNTING · p. 26

E SEMANTIC ALIGNMENT MODEL: ANALYSES

  • The alignment analysis compares SAM with a λ=0 supervised-tuning ablation that differs only by removal of the alignment loss.The analysis retrieves held-out formal statements from informal statements, including tests against close twin theorems and vacuous formalizations.Source: E SEMANTIC ALIGNMENT MODEL: ANALYSES · p. 26, §E.1 · p. 27

E.1.1 SETUP

This setup measures whether the model’s raw hidden states pair held-out informal theorems with their formal counterparts, using cosine similarity and centered views.

E.1.1 SETUP

  • The setup evaluates 150 held-out pairs, split evenly across three fields, using raw hidden states rather than the alignment-trained head.It scores informal/formal views by cosine similarity and also reports centered scores to account for shifts between the two view distributions.Source: §E.1.1 · p. 27
  • Figure 7 compares informal circles and formal triangles for 150 pairs across base, λ=0, SAM, and post-RLSF spaces.The caption identifies paired views and field coloring; compare matched with unmatched cosine similarity, and note that post-RLSF views retain a shared offset removable by centering.Source: Figure 7 · p. 28
  • Twin pairs are theorem pairs whose names and statements map through one of five specified substitutions, with token-set Jaccard similarity of at least 0.6.The setup uses up to 237 twin pairs, 120 with a held-out member.Source: §E.1.1 · p. 28

E.1.2 RETRIEVAL

Across retrieval, single-symbol twins, and vacuous formalizations, SAM’s alignment term distinguishes semantically matched Lean from alternatives that supervised tuning or type correctness alone do not distinguish.

E.1.2 RETRIEVAL

  • SAM ranks the gold formalization first for every held-out statement, including when retrieval is restricted to same-field competitors.After RLSF, retrieval reaches 90% before centering and 99% after centering.Source: §E.1.2 · pp. 28–29

E.1.3 MINIMAL PAIRS

  • SAM prefers the correct formalization over its one-substitution twin for 87% of held-out lemmas, rising to 91% after centering.The checkpoint after RLSF reaches 77%, or 85% after centering; the base and λ=0 ablation remain at chance.Source: §E.1.3 · p. 29

E.1.4 VACUOUS FORMALIZATIONS

  • The vacuous formalization retains a median 73% of file characters and is type-correct and complete, yet states nothing and fails semantic correctness.It keeps imports, context, and the lemma name while replacing the theorem and proof with True and trivial.Source: §E.1.4 · p. 29
  • SAM prefers the real formalization over the vacuous one for 99% of pairs, reaching 1.00 after centering.The base and λ=0 ablation prefer the vacuous version before centering and remain near chance afterward.Source: §E.1.4 · p. 29

E.2 GENERATION RESULTS

The direct-generation comparison evaluates SAM against Leanstral without tools, while the paper distinguishes cold-start model effects from the RL-trained systems used to measure the method.

E.2.1 FAIR COMPARISON AND SCOPE

  • The seed harness adapts the Vibe harness used to train Leanstral, while the paper treats harnesses evolved for each system as part of the comparison.Leanstral’s prior training in Vibe and the evolved harness search with Leanstral both favor the base in the harness comparison.Source: §E.2.1 · p. 29
  • The method comparison is between RL-trained systems, while SAM-versus-SFT isolates the alignment term because both share data, configuration, and batch order.The authors note supervised tuning may erode behaviors learned by prior RL.Source: §E.2.1 · pp. 29–30

E.2.2 DIRECT GENERATION

  • On 771 problems, SAM type-checks on 29.3% versus Leanstral’s 18.4%, but TC+SC is 1.4% versus 3.5%.SAM’s type-correct files that match their statements also complete their proofs, locating the gap in statement fidelity.Source: §E.2.2 · p. 30, Table 8 · p. 30
  • SAM exceeds the decoding budget before closing the code fence on 682 of 3,084 samples, versus 329 for Leanstral.RLSF trains both statement fidelity and when to stop.Source: §E.2.2 · p. 30

E.2.3 ABLATION STUDIES

The ablations separate SAM’s alignment contribution from supervised tuning, then evaluate how its representation and RL-trained harness behavior combine in agentic generation.

E.2.3 ABLATION STUDIES

  • The ablation samples use high reasoning despite training with reasoning off; missing replies count as failed attempts and lower overall pass@4.SFT returns no reply for 74.9% of samples and SAM for 37.5%, so the study also reports scores on answered problems.Source: §E.2.3 · p. 30, Table 9 · p. 30
  • SAM type-checks on 23.7% of all problems versus SFT’s 14.7%, but the alignment term raises type-correctness rather than statement fidelity.Among answered problems, type-check rates are similar, while SFT leads on TC+SC.Source: §E.2.3 · p. 30, Table 9 · p. 30

E.2.4 AGENTIC GENERATION

  • AIPROVER reaches 94.8% TC and 36.7% TC+SC with full proofs, versus 84.4% and 22.6% for Leanstral with an evolved harness.These are pass@4 results on LoCoBench-Val; the table compares the systems inside the seed and evolved harnesses.Source: §E.2.4 · p. 30, Table 10 · p. 31

E.2.5 SAM AS A COLD START FOR RLSF

  • RLSF’s reward targets statement fidelity and length, and it learns reasoning and harness behavior inside the harness.Episodes without a file score 0, below any episode that produces a written file.Source: §E.2.5 · p. 31
  • SAM supplies a representation absent from Leanstral and SFT; after RLSF it still retrieves gold formalizations for 90% of statements, or 99% after centering.AIPROVER’s full-proof semantic result is reported against Leanstral with an evolved harness, and the authors credit the stages jointly.Source: §E.2.5 · p. 31

E.3.1 TRAINING DATA

SAM is trained on 23,507 NL–FL pairs drawn from gold Mathlib and CSLib data and filtered Mizar formalizations.

E.3.1 TRAINING DATA

  • SAM uses 18,757 gold Mathlib and CSLib pairs plus 4,750 compiled, judge-aligned Mizar pairs, with no validation identifier overlap.Ten percent are held out for validation; the median pair is 668 tokens and none exceeds the 8,192-token cap.Source: §E.3.1 · p. 31

E.3.2 TRAINING

SAM trains language modeling and semantic alignment in two passes, then applies a batch alignment loss that pulls matched views together and pushes mismatched views apart. The matrix formulation weights repulsion by the probability assigned to incorrect pairings.

E.3.2 TRAINING

  • Each training step runs two passes over up to 32 pairs: one predicts formal tokens and extracts the NL view, while the other encodes the formal view alone.The batch is packed under a 24,576-token budget; the gradient of LCE + λLalign updates the adapters, alignment head, and [PRED] embedding.Source: §E.3.2 · p. 31
  • At inference, Δ is merged into the decoder; during training, LCE scores formal-token positions and Lalign aligns the two views on the unit sphere.The semantic encoder feeds Lalign, which pulls paired views together and pushes other pairs apart.Source: Figure 8 · p. 32

E.3.3 THE BATCH AS A MATRIX

  • The batch forms a B × B score matrix: diagonal entries compare each NL theorem with its own formal pair, while off-diagonal entries compare it with other formal pairs.Rows and columns give the two directions of matching probability across the batch.Source: §E.3.3 · p. 32
  • Descending the alignment loss raises diagonal scores and lowers off-diagonal scores, with repulsion weighted by the probability assigned to each incorrect pairing.The pull alone could map every view to one point, leaving equal row probabilities of 1/B and loss ln B.Source: §E.3.3 · p. 32

F HARNESSES AND PROMPTS OF AIPROVER, ITS TRAINING PIPELINE, AND THE BASELINES

This section documents AIProver’s seed and evolved harnesses, HarnessEvolve’s certificate-driven revisions, and the related training and baseline prompts and semantic judges. It describes checks and review aimed at faithful Lean formalization, including statement inference from English for theorem-and-proof and theorem-only inputs.

F.1 INITIAL AIPROVER HARNESS H0 (INFERENCE AND HARNESSEVOLVE SEED)

  • H0 wraps Mistral Vibe’s Lean agent in a fresh per-problem Mathlib environment, runs one user turn with tool calls, then recompiles and grades the Lean file; it seeds HarnessEvolve and the AIPROVER-Baseline rows.The harness uses Vibe file and shell tools plus lean-lsp tools under MCP aliases.Source: §F.1 · p. 33
  • H0’s task prompt requires a faithful Lean theorem and, when supplied, a proof following the informal proof plan; it directs the model to write and compile the theorem early.The prompt warns against weakening the statement or adding hypotheses, and treats an empty proof block as statement-only formalization with sorry.Source: §F.1 · p. 35

F.2 EVOLVED AIPROVER HARNESS (INFERENCE AND TRAINING)

  • The evolved harness retains H0’s tools, loop, and system prompt but adds four between-turn hooks for whole-file writes, gated searches, budget notices, and post-stop verification.Searches are withheld after the free-search budget if no theorem is on disk; budget notices report remaining turns or wall clock and can block exploration tools near timeout.Source: §F.2 · p. 36
  • After the model stops, verification compiles the file and can request up to three repairs; a triviality probe rejects statements closed by a fixed tactic sequence.The harness snapshots answer-file versions and leaves the newest compiling version on disk, preferring one without sorry, without rewriting the statement.Source: §F.2 · pp. 36–37
  • When a file compiles and passes the triviality probe, statement review compares the informal theorem with the Lean signature clause by clause, checking both missing and extraneous content.The review covers objects and structure, hypotheses, quantifiers, and the full conclusion, including added hypotheses or fixed values where the source quantifies.Source: §F.2 · p. 37
  • The task contract distinguishes proof-bearing inputs, which require theorem and proof, from empty-proof inputs, which require a faithful theorem with sorry; grading ranks faithful completed proofs above faithful elaborating statements with sorry, weakened statements, and non-elaborating files.It explicitly prioritizes preserving the statement over completing a proof by narrowing or weakening it.Source: §F.2 · p. 38
  • The harness directs agents to keep an actual theorem in the answer file and preserve an elaborating checkpoint, using `sorry` for unfinished proof steps and repairing compiler errors before submission.After a finite number of repair attempts, the file is accepted as it stands, so the instructions prioritize an elaborating file over an unfinished tactic block.Source: §F.2 · p. 39
  • The evolved harness checks theorem content by rejecting statements closed by automation alone, then asks the agent to compare its statement with the informal theorem clause by clause.The agent is warned to preserve the theorem’s hypotheses, quantifiers, and vocabulary rather than narrow or weaken it.Source: §F.2 · p. 39
  • For named mathematical properties, the harness instructs the agent to verify the library predicate’s definition and use that notion only when it matches the informal theorem.When the match cannot be confirmed, it recommends stating the property explicitly rather than guessing a similarly named predicate.Source: §F.2 · p. 39

F.3 AIPROVER AS A SKILL FOR CODING AGENTS (INFERENCE)

  • The coding-agent skill requires type-correct, complete, semantically correct, and proof-faithful Lean, delegating proof search to AIProver while the host plans, judges, decomposes, and weaves results.The host must judge semantic correctness and proof faithfulness because compilation alone does not establish either.Source: §F.3 · p. 40
  • On 509 hard training problems, AIProver produced 205 solved faithful formalizations and 173 additional complete compilations that stated the wrong theorem.The harness champion was selected over 10 rounds; the playbook reports one sample on the training set.Source: §F.3 · pp. 40, 42
  • When a whole-problem sample is incomplete or unfaithful, the skill has the host freeze a judged statement skeleton, delegate open proof pieces with relevant lemmas, and weave returned proofs back into it.The final gate checks type correctness and completeness, then separately applies the semantic and proof-faithfulness judge protocol.Source: §F.3 · pp. 40–41

F.4 HARNESSEVOLVE (EVOLUTIONARY SEARCH)

  • HarnessEvolve’s mutator runs a frontier coding agent headlessly once per round, using a static guide and a per-round prompt populated with parent code, certificates, rung table, lineage memory, and acceptance bar.Source: §F.4 · p. 43
  • HarnessEvolve should improve English-to-Lean inference using generalizable reasoning changes, not reference statements, problem-keyed lookup tables, or other mechanisms that encode answers.Suggested levers include restating the English claim, enumerating its quantifiers and hypotheses, searching Mathlib for standard terminology, and checking the Lean statement against its English reading.Source: §F.4 · p. 44
  • Harnesses must detect whether the proof block is empty: theorem-only inputs accept a faithful statement with sorry, while theorem-and-proof inputs require a completed proof.Checks must also reject vacuous or trivial statements and monitor suspected statement erosion, such as shortening statements or reducing Mathlib usage as compilation rises without semantic success.Source: §F.4 · pp. 44, 46
  • Semantic certificates distinguish weaker from stronger candidate statements and identify mismatches, guiding targeted harness changes without copying reference statements, names, or lemmas.When neither implication is proved, compare the statements and classify the mismatch; the scalar rung alone cannot distinguish opposite failure directions.Source: §F.4 · pp. 44, 46

F.5 SEMANTIC-CORRECTNESS JUDGES (EVALUATION)

  • Semantic correctness is judged through two comparisons: candidate Lean against the gold formalization and the candidate’s informalization against the natural-language input.The evaluation uses two frontier judges with one system prompt and separate prompts for the formal-language and natural-language comparisons.Source: §F.5 · p. 47

F.6 BASELINE AGENTS AND LLMS (INFERENCE)

  • Single-turn models, coding agents, and agentic baselines receive a common task instruction, adapted to each system’s input and output conventions.The named agentic baselines are Aristotle, Numina-Lean-Agent, and OpenGauss.Source: §F.6 · p. 48

F.7 DATA PIPELINES (DATA CURATION)

  • LoCoBench’s natural-language data uses Lean-to-natural-language prompts for Mathlib and CSLib, Mizar-to-natural-language prompts for Mizar, and separate teacher prompts for data distillation.The Lean prompt requests a proof plan, accurate theorem and proof, and preservation of proof structure; the Mizar prompt requests a self-contained mathematical account that excludes formal-system identifiers and unused machinery.Source: §F.7 · pp. 49–50
Loading 2610.05367v1…