Preprint · 2026 · arXiv:2610.05367

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

Prithwish Jana1,c Viet Bach Hoang1,† Logan Luna1,† Viresh Pati2,† Akash Singirikonda1,† Cy Xie3,†
Lisa Carbone4,§ Wuyang Chen5,§ Walter Moreira6,§ Joe Stubbs6,§ Sriram Vishwanath1,§ Vijay Ganesh1

1Georgia Institute of Technology2University of Pennsylvania3Foothill College
4Rutgers University5Simon Fraser University6University of Texas at Austin

Georgia Tech University of Pennsylvania Foothill College Rutgers University Simon Fraser University The University of Texas at Austin
arXiv Code soon BibTeX

cCorresponding author: pjana7@gatech.edu.
†Equal contribution, sorted by last name.
§Equal senior authorship, sorted by last name.

TL;DR
  • The setting. Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Research mathematics involves long chains of interdependent definitions, lemmas, and proofs often absent from libraries such as Mathlib, so recent work wraps the LLM in a harness: a stateful multi-turn loop with Lean and search tools.
  • The problem. Successful compilation does not guarantee that a translation preserves the theorem’s meaning or the proof’s reasoning, aligned NL–FL training data are scarce, and leading agents often rely on costly frontier models, manually engineered harnesses, and mathematicians in the loop.
  • Existing agents, and their limitations. LeanMarathon, Numina-Lean-Agent, OpenGauss, and the closed-source Aristotle implement the loop, and Claude Code and Codex are used directly by mathematicians. But most AFPS models are RL-trained on Lean’s binary verdict, which never compares the output with the NL input, so a formalization that compiles but proves the wrong theorem counts as success; and the agents’ harnesses are hand-built and retain the control flow of coding agents built for software engineering, which suits neither Lean proving nor open-weight models.
  • What we do instead. AIProver post-trains a 119B open-weight language model and simultaneously evolves its agentic, tool-calling harness: per round, HarnessEvolve adapts the harness control flow to the model, then RL post-trains the model within it. We contribute:
    • a semantic alignment model (SAM) fine-tuned so that an NL theorem–proof pair and its Lean counterpart are one mathematical object;
    • verifiers for type correctness, proof completeness, and semantic correctness that return graded rewards and diagnostic certificates, which drive reinforcement learning via symbolic feedback;
    • HarnessEvolve, a certificate-driven evolutionary search over the whole harness control flow that retains rejected designs as negative evidence;
    • LoCoBench, 58.9k research-level instances with a 771-instance validation split whose theorem–proof pairs have no public Lean formalization.
  • The effect. 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%, outperforming Numina-Lean-Agent and OpenGauss in that role at 24% lower cost than Numina-Lean-Agent, pushing the accuracy–cost frontier of research-level AFPS.
At a glanceProof auto-formalization of research-level mathematics: accuracy and cost, standalone and in conjunction with Codex and Claude Code
Accuracy semantic correctness, full proofs (%) Cost per attempt USD Standalone open-weight model on local GPUs OpenGauss (best open-weight system) 21.5% $0.32 AIProver 36.7% $0.32 same cost In conjunction with Codex GPT-5.6-Sol Codex alone 34.1% $0.53 Numina-Lean-Agent + Codex 44.5% $1.08 AIProver + Codex 62.4% $0.85 21% cheaper In conjunction with Claude Code Opus 5 Claude Code alone 41.9% $0.81 Numina-Lean-Agent + Claude Code 72.5% $2.03 AIProver + Claude Code 79.8% $1.55 24% cheaper

pass@4 on the 771 instances of LoCoBench-Val. Pale bars: the coding agent alone. Hollow bars: the best prior Lean agent in that role. Filled bars: AIProver. Cost is the host’s tokens at list prices plus the GPU time serving the open-weight model, per attempt over the same 3,084 attempts.

01 · Use it

A Lean specialist, standalone or in conjunction with frontier coding agents

AIProver is designed to serve standalone, as an open-source platform making research-level formalization accessible to all, and in conjunction with frontier agents, as a Lean specialist pushing their accuracy–cost frontier. It can be used in three ways.

StandaloneCommand-line agent

The post-trained Leanstral-1.5 inside the evolved harness, at GPU cost only: the model on a GPU server, the harness and the Lean toolchain on your machine.

36.7% pass@4 semantic correctness at $0.32 per attempt
Codex skillLean specialist inside Codex

Codex plans, delegates the Lean work to AIProver, judges faithfulness, decomposes, and weaves.

62.4% vs. 34.1% for Codex alone, at $0.85 per attempt
Claude Code skillLean specialist inside Claude Code

Claude Code plans, delegates the Lean work to AIProver, judges faithfulness, decomposes, and weaves.

79.8% vs. 41.9% for Claude Code alone, at $1.55 per attempt
How the two work togetherThe host plans and judges; AIProver writes Lean and searches for proofs
Host coding agentClaude Code or Codex: plans, delegates, judges
  • Reads the natural-language theorem and proof and plans the formalization: the definitions, the theorem parts with their exact hypotheses, the intermediate lemmas.
  • Hands the whole problem to AIProver and waits for the candidates.
  • Judges every returned file: does the statement say the same theorem, does the proof follow the paper’s argument? Fixes statements when needed.
  • If no candidate passes, splits the problem into lemmas, sends each to AIProver, and weaves the returned proofs into one file.
ToolsAIProver’s command line (submit, wait, result, check) and the lean-lsp tools for small local checks such as reading a goal or confirming a lemma name. It never searches for proofs itself.
AIProverThe Lean specialist: writes Lean, searches for proofs
  • Each call is a full multi-turn session of the post-trained model inside its evolved harness, several samples in parallel.
  • Writes the Lean statement and proof, compiles, reads Lean’s errors, searches Mathlib, and repairs until the file type-checks.
  • Returns each candidate with its checks: type-correct and complete, or where it fails.
ToolsLean 4 with Mathlib, the lean-lsp tools (goal states, diagnostics, lemma search), and its verifiers. The model runs on a GPU server; the harness and Lean run on your machine.

A session ends when the final file type-checks and is complete, and the host has judged it semantically correct and faithful to the paper’s proof.

02 · Problem

Research mathematics needs an affordable, autonomous auto-formalizer

Auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean. Research mathematics involves long chains of interdependent definitions, lemmas, and proofs often absent from libraries such as Mathlib, so recent agents wrap the LLM in a harness, a stateful multi-turn loop with Lean and search tools. These agentic systems share five limitations.

  1. CostClaude’s FLT formalization took eleven days and six billion output tokens, resources at frontier rates beyond typical academic budgets.
  2. Human-in-the-loop dependenceMathematicians supplied Fermat’s FL target statements and stayed involved, Gauss ran on an expert-built, iteratively-refined harness, and Meta’s AutoformBot, with 26 textbooks formalized, calls human involvement essential.
  3. Jagged intelligenceFrontier models excel at many tasks yet falter on unfamiliar ones; expert review of Claude’s formalization found strong local proof repair but poor definitions and interfaces, and no model proves over 20% of ArXivLean’s recent research theorems.
  4. Semantic driftOutput cannot be trusted as-is. Lean checks the FL proof against the FL theorem, not the NL one, so compiled code may prove the wrong theorem or silently patch a flawed NL proof step.
  5. Lack of accessibilityHeadline results often rest on non-public models: FLT and Navier–Stokes reportedly used internal ones, so the auto-formalization and proof synthesis (AFPS) process cannot be cross-checked.
The goalAn affordable, autonomous AI agent for semantically correct and faithful proof auto-formalization of research-level mathematics. Given NL research text interleaving theorems and proofs, it should (i) produce a full Lean counterpart preserving each theorem’s meaning and proof’s reasoning, (ii) run unattended, (iii) use an open-weight model via a model-agnostic training and harness recipe, and (iv) be a sub-agent or skill of frontier agents. It should serve standalone as an open-source platform making research-level formalization accessible to all, and in conjunction with frontier agents as a Lean specialist pushing their accuracy–cost frontier, since frontier models will likely stay the most expensive for the foreseeable future.
Proof auto-formalization: the NL theorem and proof map to a Lean theorem and proof; Lean checks type-correctness and completeness, a judge checks semantic correctness and proof faithfulness.
Proof auto-formalization. Lean checks (a) and (b); a judge checks (c) and (d).

The task, under four properties

Given an NL theorem TNL and its proof PNL, produce an equivalent Lean pair.

  • (a) Type-correctness. Lean’s kernel accepts the formalization.
  • (b) Completeness. The proof uses no placeholder such as sorry, admit or an empty by block.
  • (c) Semantic correctness. The formal theorem states exactly TNL, neither adding assumptions nor dropping conditions.
  • (d) Proof faithfulness. The formal proof follows the strategy of PNL, including its intermediate lemmas.

Four issues, four answers

Issue 1 · NL–FL semantic alignment

Next-token fine-tuning never teaches an LLM that an NL theorem and its FL counterpart are the same mathematical object in two syntactic forms.

Semantic Alignment Model (SAM). A contrastive term aligns the NL and FL views inside the LLM.
Issue 2 · Fine-grained training signal

RL on Lean’s binary verdict never compares the output with the NL input, so a formalization that compiles but proves the wrong theorem counts as success.

Reward ladder with certificates. Four verifier checks return a graded reward and a certificate, so RL and harness search learn from partial success.
Issue 3 · Research-level training data

Gold NL–Lean theorem–proof pairs barely exist: ShadowBench (178) and ArXivLean (41) are evaluation sets; Mizar holds decades of verified research mathematics, in neither NL nor Lean.

LoCoBench. 58.9k instances, with a 771-instance validation split that has no Lean formalization online.
Issue 4 · AFPS-tailored harness design

LeanMarathon and Numina-Lean-Agent retain the control flow of coding agents built for software engineering, and hand-tailoring a harness takes months.

HarnessEvolve. A certificate-driven evolutionary search over the whole harness control flow, re-run as the model changes.

03 · Approach

AIProver post-trains the model and evolves the harness together

Definition · agents and harnessesAn agent A = ⟨M, H⟩ pairs an LLM M with a harness H, the software layer that executes the actions M proposes and governs the agent’s context, tools, memory, and control flow. AIProver optimizes the full agent: it post-trains M and evolves H.
WalkthroughModel and harness are optimized together: each round evolves the harness for the current model, then post-trains the model in it
Overall post-training loop of AIProver: Phase 1 bootstraps the harness with HarnessEvolve and the model with SAM fine-tuning; Phase 2 interleaves RLSF post-training and HarnessEvolve for K rounds.
  1. The initial agentA0 = ⟨M0, H0⟩: Leanstral-1.5 as M0, and a seed harness H0 adapted from Mistral’s Vibe with lean-lsp-mcp.
  2. Phase 1 · HarnessEvolveBootstrap the harness: evolve H0 into H1 under M0. HarnessEvolve optimizes the whole control flow of the harness in an evolutionary search.
  3. Phase 1 · SAM fine-tuningBootstrap the model: SAM-tune M0 into M1. SAM aligns NL and FL pairs in the LLM.
  4. Phase 2 · HarnessEvolveWith Mi frozen, evolve Hi into Hi+1, re-tailoring the harness to the current model. Harness and model use disjoint training subsets.
  5. Phase 2 · Agentic RLSFWith Hi+1 frozen, RLSF post-trains Mi into Mi+1 on graded verifier reward, learning from partial successes.
  6. Repeat K rounds, gated⟨Mi+1, Hi+1⟩ is kept only if its held-out fitness improves, else rolled back.
  7. Click a step to jump to it.

04 · Components

One graded reward and one certificate drive both the model’s and the harness’s search

Four checks, each presupposing the previous one, return a value and a certificate. The reward is RLSF’s per-rollout signal and, averaged over tasks, a harness’s fitness; the certificate is what HarnessEvolve’s mutator reads.

(1) Type-correctness · TCLean accepts the file: every definition and tactic step resolves and the kernel type-checks the proof term.Certificate: Lean’s diagnostics verbatim.
(2) Completeness · CPNo sorry, and no axioms beyond Lean’s standard ones (#print axioms).Certificate: the placeholder or the violating axiom.
(3) Semantic correctness · SCLogical equivalence to the gold theorem, proved in each direction with an extended BEq+: one direction gives vSC = 0.5, both give 1.Certificate: both verdicts.
(4) Length fidelity · LFHow close the proof’s length is to the gold one: a far shorter proof relies on heavy automation, a longer one meanders.Certificate: the length ratio.
OutcomeTCCPSCReward r
No answer–––0
Ill-typed✗––0.05
Incomplete proof✓✗vSC0.15 + 0.35 vSC
Complete proof✓✓vSC0.30 + 0.60 vSC
Solved✓✓✓1 − 0.10 (1 − vLF)

Reward ladder (Table 1 of the paper). A matched theorem outweighs completeness, as a flawless proof of the wrong theorem is not useful. The certificate lists the checks in ladder order, so the first failing check is the first to fix.

SAM fine-tuning: two forward passes give an NL view and an FL view, aligned by a contrastive loss alongside the language-modeling loss.
SAM: contrastive NL–FL alignment.

Model · cold start

Semantic Alignment Model (SAM)

  • A decoder-only LLM fine-tuned to represent MNL and MFL as the same mathematical object, which language modeling alone does not induce.
  • A contrastive term, optimized jointly with the language-modeling loss, aligns the two views in a shared semantic space; SAM remains a generative LLM.
  • Two forward passes yield the two views: the state at a reserved [PRED] token after the NL text, and the final state of the Lean text alone.
  • Effect. The cosine of matched NL–FL pairs rises from 0.11 to 0.75; RLSF mostly keeps it (0.64).

Harness · search

HarnessEvolve

  • Evolves the harness while the model stays frozen. A harness is a program, so the search space is countably infinite.
  • The search memory is a tree rooted at the current harness: each node a harness with its fitness, certificates, and verdict; each edge the source diff that produced the child.
  • Every evaluated harness is kept, accepted or rejected, so the mutator learns which changes raised fitness and which to avoid, as conflict-driven clause learning does in SAT solvers.
HarnessEvolve: a search-memory tree of accepted and rejected harnesses; parent selection, mutation by a coding agent, rollout, and acceptance.
HarnessEvolve search.
  1. Parent selectionAn upper-confidence rule, as in UCB1 and UCT, balances exploiting high-fitness nodes against exploring rarely expanded ones.
  2. MutationA frontier coding agent rewrites the parent into a child, guided by the certificates and by which edits in the tree raised fitness.
  3. Rollout and fitnessThe child runs on every training instance, k times each; the fitness is the mean reward.
  4. Child acceptanceAccepted if it beats the best fitness so far, else rejected; kept in memory either way. After R rounds, the best harness goes to RLSF.
Agentic RLSF: multi-turn rollouts inside the frozen harness are scored by symbolic verifiers and optimized with GRPO.
Agentic RLSF: post-training on verifier reward.

Model · post-training

Agentic reinforcement learning via symbolic feedback

  • An episode is one run of the agent inside the frozen harness: reasoning, tool calls, and observations, turn after turn.
  • Only the Lean file it finally writes is rewarded, by sound symbolic tools, the Lean kernel and BEq+, instead of a learned reward model.
  • Optimized with GRPO; the objective applies only to tokens the model generated.
  • Why the ladder matters. Under a binary verification reward, a group whose rollouts all fail or all succeed yields no gradient; the ladder separates ill-typed, incomplete, and complete proofs even within a failing group.

05 · Benchmark

LoCoBench: 58.9k research-level instances, 771 of them with no Lean formalization online

Research-level mathematics in three fields: algebraic structures, foundations, logic & complexity, and number theory.

Data curation for LoCoBench: dependency analysis of the Lean and Mizar libraries and of the textbook, then informalization with semantic-equivalence feedback into LoCoBench-Train and LoCoBench-Val.
Data curation for LoCoBench-Train and LoCoBench-Val. Mathlib, CSLib, Mizar, and textbook theorem–proof pairs become standalone NL–FL instances.
SourcesMathlib and CSLib (18.8k Lean theorem+proof pairs, one standalone type-checked .lean file each), the Mizar Mathematical Library (40.1k pairs, one .miz file per theorem), and the 71 theorems of a bounded-arithmetic textbook.
InformalizationLLMs informalize far more accurately than they formalize. Each file is informalized by a coding agent in a feedback loop with CriticLeanGPT, an NL–FL faithfulness judge, until it passes.
Train/Val splitVal is out of distribution: the 100 longest-proof Mizar theorems per domain, from papers disjoint from Train, plus the 71 textbook theorems. Val proofs are about 8× ProofNet’s.
DistillationLean labels for the remaining Mizar theorems in Train are distilled from a teacher model with verifier feedback: each must compile and pass a semantic check.
DomainTrain: Mathlib+CSLibNL + LeanTrain: MMLNL onlyValNL onlyTotal
Algebraic structures28,432
Ring theory6,8413,303100
Group theory3,31014,778100
Foundations, logic & complexity14,010
Set theory2,871555100
Logic1,2832,637100
Computability9383,579100
Model theory819857100
Bounded arithmetic (textbook)––71
Number theory16,471
Number theory2,69513,676100
Total18,75739,38577158,913

LoCoBench composition (Table 2 of the paper). Mathlib+CSLib entries carry gold Lean; MML entries are NL-only.

06 · Results

Against 39 systems, AIProver beats every open-weight system standalone and lifts the frontier coding agents it serves

Pass@4 on LoCoBench-Val (771 instances) under three nested criteria: TC, the file compiles; TC+SC, the statement is also semantically correct; and TC+SC with full proofs, which also requires completeness. All 39 systems, in four families, per field and overall.

SystemAlgebraic structuresn = 200Foundations, logic & complexityn = 471Number theoryn = 100Overalln = 771
TCTC+SCFullTCTC+SCFullTCTC+SCFullTCTC+SCFull
AFPS models, single-turn
Kimina-Autoformalizer-7B52.03.50.057.31.10.080.026.00.058.94.90.0
StepFun-Formalizer-7B16.05.50.09.81.50.051.026.00.016.75.70.0
Goedel-Prover-V2-32B29.50.00.056.50.60.622.00.00.045.00.40.4
DeepSeek-Prover-V2-7B10.00.00.012.70.20.27.00.00.011.30.10.1
Kimina-Prover-Distill-8B13.01.01.015.10.60.615.010.010.014.51.91.9
Kimina-Prover-RL-1.7B1.50.50.51.50.00.08.07.07.02.31.01.0
Kimina-Autoformalizer-7B → Goedel-Prover-V2-32B14.51.01.024.40.20.232.010.010.022.81.71.7
Kimina-Autoformalizer-7B → DeepSeek-Prover-V2-7B16.01.51.522.70.20.234.011.010.022.41.91.8
Kimina-Autoformalizer-7B → Kimina-Prover-Distill-8B12.01.01.023.40.80.828.012.012.021.02.32.3
StepFun-Formalizer-7B → Goedel-Prover-V2-32B10.03.03.06.20.80.818.012.08.08.72.92.3
StepFun-Formalizer-7B → DeepSeek-Prover-V2-7B18.55.50.010.61.50.056.026.01.018.55.70.1
StepFun-Formalizer-7B → Kimina-Prover-Distill-8B18.55.52.010.61.50.456.026.03.018.55.71.2
AFPS agents, multi-turn
StepFun-Formlzr.-7B → Axiom AXLE (w/ GPT-OSS-120B)18.55.54.513.81.30.861.029.012.021.16.03.2
StepFun-Formlzr.-7B → Hilbert17.56.05.010.61.10.656.027.017.018.35.73.9
Leanstral-1.5-119B-A6B (no tools)16.55.54.520.22.32.114.05.04.018.43.53.0
Leanstral-1.5-119B-A6B (w/ tools)21.014.514.529.310.210.231.020.020.027.412.612.6
Aristotle43.025.025.042.913.613.445.029.029.043.218.518.4
Math-Inc OpenGauss (w/ Leanstral-1.5-119B-A6B)62.029.028.554.815.114.960.042.039.057.322.221.5
+ Codex (w/ GPT-5.5)92.523.523.596.616.816.690.032.032.094.720.520.4
+ Codex (w/ GPT-5.6-Sol)99.559.058.598.529.929.999.066.065.098.842.241.9
+ Claude Code (w/ Claude-Opus-4.7)99.546.043.099.216.615.999.055.050.099.229.227.4
+ Claude Code (w/ Claude-Opus-5)98.067.567.599.445.045.099.073.072.099.054.554.3
Numina-Lean-Agent + Codex (w/ GPT-5.6-Sol)100.056.056.0100.036.135.9100.062.062.0100.044.644.5
+ Claude Code (w/ Claude-Opus-5)100.077.077.0100.070.170.1100.076.075.0100.072.672.5
Foundation models, single-turn
Qwen3-Coder-30B-A3B0.00.00.01.50.20.21.01.00.01.00.30.1
Gemma-3-27B0.00.00.01.90.20.21.00.00.01.30.10.1
Qwen3-Coder-Next (80B-A3B)3.00.50.51.30.20.20.00.00.01.60.30.3
Llama-4-Maverick-17B-128E1.01.01.04.71.31.33.02.02.03.51.31.3
DeepSeek-V3.2 (685B)2.52.02.05.92.32.34.02.02.04.82.22.2
GPT-OSS-20B33.03.53.561.42.12.130.07.06.049.93.13.0
GPT-OSS-120B20.55.05.042.53.23.021.03.03.034.03.63.5
GPT-5.570.529.529.576.920.020.066.040.040.073.825.025.0
GPT-5.6-Sol55.527.527.567.521.421.462.038.038.063.725.225.2
Claude-Opus-4.780.017.014.593.88.77.683.035.022.088.814.311.3
Claude-Opus-585.529.029.092.817.016.881.040.040.089.423.123.0
Coding agents, multi-turn
Codex (w/ GPT-5.5)72.533.532.568.614.414.474.043.043.070.323.122.8
Codex (w/ GPT-5.6-Sol)95.045.545.098.524.023.694.063.062.097.034.634.1
Claude Code (w/ Claude-Opus-4.7)90.022.519.594.910.69.392.044.031.093.318.014.8
Claude Code (w/ Claude-Opus-5)89.554.554.594.333.333.388.057.057.092.241.941.9
Proposed (ours)
AIProver-Baseline (model = Leanstral-1.5-119B-A6B)
w/ Seed Harness59.524.520.054.611.710.468.049.032.057.619.815.7
w/ HarnessEvolve90.037.528.080.918.515.790.059.044.084.428.722.6
AIProver (SAM + Interleaved RL/HarnessEvolve)97.550.050.093.824.624.694.085.067.094.839.036.7
+ Codex (w/ GPT-5.6-Sol)95.085.585.5100.046.146.1100.093.093.098.762.462.4
+ Claude Code (w/ Claude-Opus-5)100.095.095.0100.070.770.7100.092.092.0100.079.879.8

Table 3 of the paper: pass@4 (%) per field and overall. TC: the file compiles. TC+SC: the statement is also semantically correct, with or without sorry. Full: TC+SC with full proofs, i.e. complete. Bold = best, underline = second best per column.

As a standalone agent
  1. Existing open-weight models are far from research-level AFPS without a Lean-tailored harness. Every open-weight AFPS or foundation model stays below 3.9% TC+SC; AIProver raises this nearly tenfold to 36.7%.
  2. It outperforms frontier LLMs and agents. GPT-5.6-Sol (25.2%), Aristotle (18.4%), and Codex (34.1%); only Claude Code (41.9%) is higher.
  3. The gain is from post-training and the evolved harness. From the same Leanstral-1.5 base, it outperforms OpenGauss on each field (36.7% vs. 21.5%), and its 67.0% on number theory is above Codex (62.0%) and Claude Code (57.0%).
As a skill for frontier coding agents
  1. AIProver lifts both hosts more than prior harnesses. Claude Code goes from 41.9% to 79.8% (vs. 72.5% with Numina-Lean-Agent, 54.3% with OpenGauss) and Codex from 34.1% to 62.4% (vs. 44.5%, 41.9%).
  2. The gain comes from AIProver, rather than the host. It adds 28.3% to Codex and 37.9% to Claude Code, whereas Numina-Lean-Agent adds 10.4% and 30.6% and OpenGauss 7.8% and 12.4%, so the weaker host gains almost three times more from AIProver than from either prior agent.

Ablation

What does each component add?

Leanstral-1.5 w/ tools27.4% TC12.6% full proofsThe base model with Lean tools, before any AIProver component.
+ seed harness57.6% TC15.7% full proofsWrapping M0 in H0.
+ HarnessEvolve84.4% TC22.6% full proofsEvolving H0 at fixed M0: the harness alone mostly fixes compilation, motivating post-training.
+ SAM, interleaved RLSF/HarnessEvolve94.8% TC36.7% full proofsPost-training in the evolved harness.

07 · Analysis

Inside SAM’s aligned space

SAM’s role is the aligned space that initializes RLSF and HarnessEvolve. Two views of that space: 150 held-out pairs, and four related training lemmas.

Informal and formal views of 150 held-out pairs in the first three principal components of four models: the base and the λ = 0 (SFT) ablation form two separate clouds; in SAM each informal view sits near its own formal view; after RLSF the matched views stay paired with a shared offset.
The aligned space in raw views. Informal (circles) and formal (triangles) views of 150 held-out pairs, each pair joined, colored by field. In the base and the λ = 0 (SFT) ablation the two views form separate clouds and a matched pair is no closer than an unmatched one (cosine 0.11 against 0.11, and 0.13 against 0.12). In SAM each informal view sits near its own formal view (0.75 against 0.32 unmatched) and the space is organized by field. After RLSF the matched views are separated by a shared offset and stay paired (0.64 against 0.31).

Relations between lemmas carry across the two languages

Four Mathlib lemmas about pre-games, related by two substitutions (multiplicative to additive, commutative to associative), in SAM’s head space. Each lemma’s Lean and English views nearly coincide, so the views form matching parallelograms, with edge cosines 0.74 and 0.78 in the full space.

Four related Mathlib lemmas: their Lean and English views in SAM's head space form matching parallelograms.
Four related lemmas in SAM’s semantic encoder. Solid edges: multiplicative to additive; dashed: commutative to associative; dotted lines join the two views of a lemma.

08 · Cost

Higher accuracy at lower cost

Cost per attempt over the same 3,084 attempts: the host coding agent’s tokens at list prices, plus the GPU time that serves the open-weight model.

CostAIProver forms the accuracy–cost Pareto frontier
costlier and less accurate than AIProver 20 40 60 80 0 0.5 1 1.5 2 Cost per attempt (USD) TC+SC, full proofs (%) 36.7%$0.32 62.4%$0.85 79.8%$1.55
Host (symbol):standaloneCodex (GPT-5.6-Sol)Claude Code (Opus 5)
Lean agent (shape):AIProverNumina-Lean-AgentOpenGauss
  1. Frontier coding agents aloneCodex (GPT-5.6-Sol) reaches 34.1% at $0.53 per attempt; Claude Code (Opus 5) 41.9% at $0.81.
  2. Prior Lean agentsStandalone, OpenGauss reaches 21.5% at $0.32, GPUs only. As skills, Numina-Lean-Agent and OpenGauss lift both hosts at a higher cost per attempt: 44.5% at $1.08 and 41.9% at $1.05 with Codex; 72.5% at $2.03 and 54.3% at $1.80 with Claude Code.
  3. AIProver36.7% at the same $0.32 standalone; 62.4% at $0.85 with Codex; 79.8% at $1.55 with Claude Code: more accurate and cheaper than Numina-Lean-Agent in both roles. Every other configuration lies in the shaded region, costlier and less accurate than AIProver, so AIProver forms the accuracy–cost Pareto frontier.
  4. Click a step to jump to it.

Hover a point for its configuration.

Standalone36.7%at $0.32 per attemptOpenGauss: 21.5% at the same $0.32. Both run their models on local GPUs.
With Codex62.4%at $0.85 per attemptNumina-Lean-Agent: 44.5% at $1.08. OpenGauss: 41.9% at $1.05. More accurate and 21% and 19% cheaper.
With Claude Code79.8%at $1.55 per attemptNumina-Lean-Agent: 72.5% at $2.03. OpenGauss: 54.3% at $1.80. More accurate and 24% and 14% cheaper.

The host coding agent offloads Lean work to AIProver, a Lean-specialist sub-agent on local GPUs, so it spends fewer tokens and gains accuracy.

09 · Cite

BibTeX

If you find AIProver or LoCoBench useful in your research, please cite the paper.

@article{jana2026aiprover,
  title   = {{AIProver}: Agentic Auto-Formalization of Mathematical Research via
             Certificate-Driven Evolving Harness},
  author  = {Jana, Prithwish and Hoang, Viet Bach and Luna, Logan and Pati, Viresh and
             Singirikonda, Akash and Xie, Cy and Carbone, Lisa and Chen, Wuyang and
             Moreira, Walter and Stubbs, Joe and Vishwanath, Sriram and Ganesh, Vijay},
  journal = {arXiv preprint arXiv:2610.05367},
  year    = {2026},
  url     = {https://arxiv.org/abs/2610.05367}
}