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

cs.LOOct 4, 2026

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

Authors: Prithwish Jana, Viet Bach Hoang, Logan Luna, Viresh Pati, Akash Singirikonda, Cy Xie, Lisa Carbone, Wuyang Chen, +4 more

Organizations: Georgia Institute of Technology, USA · University of Pennsylvania, USA · Foothill College, USA · Rutgers University, USA · Simon Fraser University, Canada · University of Texas at Austin, USA

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: Pipeline of AIProver . (a) LoCoBench: Mathlib, CSLib, Mizar, and textbook theorem–proof pairs as standalone NL–FL instances. (b) Model and harness are optimized together: each round evolves the harness for the current model, then post-trains the model in it. (c) SAM aligns NL and FL pairs in the LLM. (d) HarnessEvolve optimizes the whole control flow of the harness in an evolutionary search. (e) RLSF post-trains on graded verifier reward, learning from partial successes.

Panel of Figure 2 — Figure 2: Proof auto-formalization. Lean checks (a) and (b); a judge checks (c) and (d).

Outcome	TC	CP	SC	Reward ( $r$ )
No answer	–	–	–	$0$
Ill-typed	$\times$	–	–	$0.05$
Incomplete proof	✓	$\times$	$v_{\mathrm{SC}}$	$0.15+0.35\,v_{\mathrm{SC}}$
Complete proof	✓	✓	$v_{\mathrm{SC}}$	$0.30+0.60\,v_{\mathrm{SC}}$
Solved	✓	✓	✓	$1-0.10\,(1-v_{\mathrm{LF}})$

Table 1: Reward Ladder. Reward

r

of a candidate

\smash[t]{\widehat{M}_{\mathrm{FL}}}=\langle\smash[t]{\widehat{T}_{\mathrm{FL}}},\smash[t]{\widehat{P}_{\mathrm{FL}}}\rangle

per outcome of the four checks;

v_{\mathrm{TC}},v_{\mathrm{CP}}\in\{0,1\}

v_{\mathrm{SC}}\in\{0,0.5,1\}

v_{\mathrm{LF}}\in(0,1]

; ✓/

\times

denote

1

0

	Algebraic Structures ( $n$ =200)			Foundations, Logic & Complexity ( $n$ =471)			Number Theory ( $n$ =100)			Overall ( $n$ =771)
Model Name	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC
		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)
AFPS Models (single-turn)
Kimina-Autoformalizer-7B	52.0	3.5	0.0	57.3	1.1	0.0	80.0	26.0	0.0	58.9	4.9	0.0
StepFun-Formalizer-7B	16.0	5.5	0.0	9.8	1.5	0.0	51.0	26.0	0.0	16.7	5.7	0.0
Goedel-Prover-V2-32B	29.5	0.0	0.0	56.5	0.6	0.6	22.0	0.0	0.0	45.0	0.4	0.4

Table 3: Proof auto-formalization on LoCoBench-Val: AIProver vs. 39 SoTA systems. Pass@4 (%) per field and overall (shaded columns) under the metrics of Sec. 5.2 : TC (compiles), TC+SC w/ or w/o sorry (also semantically correct), and TC+SC full proofs (complete). Bold / underline = best/second best per column.

Panel of Figure 4 — Figure 4: Cost efficiency. AIProver forms the accuracy–cost Pareto frontier.

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 5: Data distillation pipeline.

Domain	Attempted	Compiles	Rate	BEq +	Rate	Aligned	Rate
Algebraic Structures	10,151	8,850	87.18%	6,531	73.83%	7,410	83.75%
Foundations & Logic	5,911	5,409	91.51%	4,372	80.89%	4,524	83.68%
Number Theory	2,685	2,311	86.07%	1,597	69.10%	1,810	78.32%
Total	18,747	16,570	88.39%	12,500	75.47%	13,744	82.97%

Appendix

Table 4: Mathlib-set distillation with Claude Opus 5, by domain. BEq + is computed against the gold formal statement; Aligned is the FormalRx-8B judge verdict, reported for comparison.

Domain	Attempted	Compiles	Rate	Aligned	Rate
Algebraic Structures	17,987	3,722	20.69%	1,282	34.70%
Foundations & Logic	7,628	1,604	21.03%	472	29.52%
Number Theory	13,508	4,102	30.37%	2,996	73.22%
Total	39,123	9,428	24.10%	4,750	50.61%

Appendix

Table 5: Mizar-set distillation with DeepSeek-V4-Flash, by domain. No gold formal statement exists for this split, so alignment is judged by FormalRx-8B against the informal statement.

System	Backbone	Input	Cache write	Cache read	Output	Turns / attempt	Time / attempt (s)	Total USD
Numina-Lean-Agent + Claude Code	Claude-Opus-5	0.08	210.3	2,882.2	100.5	15.3	432	5,267
Claude Code	Claude-Opus-5	0.01	38.1	80.7	88.8	1.8	303	2,498
Codex	GPT-5.6-Sol	2.82	125.4	1,294.5	24.3	9.3	94	1,642

Appendix

Table 6: Tokens, time, and cost of the agentic systems on LoCoBench-Val (771 instances

\times

4 attempts). Tokens in millions. Cost is computed from token counts at the rates in the text, not read from an invoice.

Panel of Figure 6 — Figure 6: Four related lemmas in SAM’s semantic encoder. (a) Four Mathlib lemmas about pre-games, related by two substitutions, multiplicative to additive and commutative to associative. Lean is shown verbatim without the file header and English as excerpts. (b) Their Lean and English views in SAM’s head space, projected on three directions estimated from the eight points. Each lemma’s two views nearly coincide, so the relations between the lemmas carry across the two languages and the views form matching parallelograms, whose corresponding edges have cosine $0.74$ for multiplicative to additive and $0.78$ for commutative to associative in the full space. Solid edges are multiplicative to additive, dashed edges commutative to associative, and dotted lines join the two views of a lemma. Labels drop the suffix _equiv . The lemmas are training pairs, shown for illustration.

Figure 7: 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 first three principal components of each model’s raw space. In the base (left) and the

\lambda{=}0

ablation (second) the informal and formal views form two 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 (third) each informal view sits near its own formal view (cosine

0.75

against

0.32

unmatched) and the space is organized by field. After RLSF (right) the matched views are separated by a shared offset and stay paired (cosine

0.64

against

0.31

), and removing the offset restores R@1 to

0.99

	Retrieval			Cosine		Minimal pairs	Vacuous
Model Name	R@1	R@5	R@1, same field	matched	unmatched	accuracy	accuracy
Leanstral-1.5-119B-A6B	0.01	0.04	0.02	0.11	0.11	0.46	0.00
SFT ( $\lambda{=}0$ )	0.01	0.03	0.02	0.13	0.12	0.54	0.00
SAM ( $\lambda{=}1$ )	1.00	1.00	1.00	0.75	0.32	0.87	0.99
SAM $+$ RLSF	0.90	0.98	0.91	0.64	0.31	0.77	0.76

Appendix

Table 7: Matching informal and formal pairs in the decoder’s hidden states , on

150

held-out Mathlib/CSLib pairs with gold Lean (

50

per field). The informal view is the final-layer state at [PRED] appended after

M_{\mathrm{NL}}

(for the base, which never saw [PRED] , the last prompt token), and the formal view is the final-layer state at the last token of

M_{\mathrm{FL}}

encoded alone. Retrieval ranks each

M_{\mathrm{NL}}

against all

150

gold formal pairs, with same-field R@1 ranking only against the

50

pairs of its field (chance

0.007

for R@1,

0.033

for R@5, and

0.02

for same-field R@1). Cosine is the mean

s(M_{\mathrm{NL}},M_{\mathrm{FL}})

over the

150

matched pairs and over all unmatched combinations. Minimal pairs is the fraction of

129

held-out twin lemmas with

s(M_{\mathrm{NL}},M_{\mathrm{FL}})>s(M_{\mathrm{NL}},M_{\mathrm{FL}}^{\prime})

, where the twin

M_{\mathrm{FL}}^{\prime}

itself may be a training pair, and vacuous is the fraction of the

149

held-out pairs with

s(M_{\mathrm{NL}},M_{\mathrm{FL}})>s(M_{\mathrm{NL}},M_{\mathrm{FL}}^{\varnothing})

(chance

0.5

for both). Bold / underline = best/second best per column, except for cosine.

	Algebraic Structures ( $n$ =200)			Foundations, Logic & Complexity ( $n$ =471)			Number Theory ( $n$ =100)			Overall ( $n$ =771)
Model Name	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC
		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)
Leanstral-1.5-119B-A6B (no tools)	16.5	5.5	4.5	20.2	2.3	2.1	14.0	5.0	4.0	18.4	3.5	3.0
SAM ( $\lambda{=}1$ )	19.5	1.5	1.5	35.9	0.6	0.6	18.0	5.0	5.0	29.3	1.4	1.4

Appendix

Table 8: Direct generation on LoCoBench-Val, no tools. Pass@4 (%) over all

771

problems on the three nested criteria of section 5.2 , per field and overall, as in table 3 . Bold = better of the two per column.

	Algebraic Structures ( $n$ =200)			Foundations, Logic & Complexity ( $n$ =471)			Number Theory ( $n$ =100)			Overall ( $n$ =771)			Overall, answered problems (at least one non-empty reply)
Model Name	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	$n$	TC	TC+SC	TC+SC
		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)			(w/ or w/o sorry)	(full proofs)
SFT ( $\lambda{=}0$ ), high	9.5	3.0	3.0	17.6	1.1	1.1	11.0	8.0	6.0	14.7	2.5	2.2	462	24.5	4.1	3.7
SAM ( $\lambda{=}1$ ), high	23.0	1.5	1.5	24.8	1.1	1.1	20.0	4.0	4.0	23.7	1.6	1.6	678	27.0	1.8	1.8

Appendix

Table 9: Ablation on

\lambda

. Setting

\lambda{=}0

removes the alignment term and recovers SFT on the same data, configuration, and batch order. Pass@4 (%) over all

771

problems on the three nested criteria of section 5.2 , per field and overall, with high reasoning, temperature

1.0

, and a

32{,}000

-token budget. The last group restricts the overall scores to the problems with at least one non-empty reply, whose number is given in the first column of the group. Bold = better of the two per column.

	Algebraic Structures ( $n$ =200)			Foundations, Logic & Complexity ( $n$ =471)			Number Theory ( $n$ =100)			Overall ( $n$ =771)
Model Name	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC	TC	TC+SC	TC+SC
		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)		(w/ or w/o sorry)	(full proofs)
Seed harness
AIProver-Baseline w/ Seed Harness	59.5	24.5	20.0	54.6	11.7	10.4	68.0	49.0	32.0	57.6	19.8	15.7
AIProver-SAM w/ Seed Harness	28.5	5.0	4.0	28.9	2.1	1.9	43.0	17.0	9.0	30.6	4.8	3.4
HarnessEvolve

Appendix

Table 10: Agentic generation on LoCoBench-Val. Pass@4 (%) over all

771

problems on the three nested criteria of section 5.2 , per field and overall, as in table 3 , for Leanstral ( AIProver -Baseline) and SAM under the seed harness and under a harness evolved for Leanstral. Bold = better of the two per column within each harness.

Panel of Figure 8 — Figure 8: SAM training and inference , in the notation of section 4.1 . (a) The two training passes. The language modeling head is scored by $\mathcal{L}_{\mathrm{CE}}$ on the FL positions, and the semantic encoder $g_{\phi}$ feeds $\mathcal{L}_{\mathrm{align}}$ , which pulls each pair’s two views together on the unit sphere and pushes other pairs apart. (b) Inference, with $\Delta$ merged into the decoder.

Explore similar work

May 19, 2026cs.LO

Pseudo-Formalization for Automatic Proof Verification

Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.

Slim Barkallah, Luke Bailey, Kaiyue Wen +2

Stanford University

Proof Formalization

Ask PDF

Jun 30, 2026cs.AI

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on five papers from the ACM Symposium on Theory of Computing (STOC) spanning combinatorics, communication complexity, mechanism design, and learning theory, successfully formalizing their main theorems and validating the generated formalizations with human experts; for all five we also formalize the proofs alongside the statements, and notably two of them are proved with no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv .

Arshia Soltani Moakhar, Iman Gholami, Max Springer +2

Autoformalization Theorem Proving Agentic Framework

Ask PDF

May 17, 2026cs.CL

OProver: A Unified Framework for Agentic Formal Theorem Proving

Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OProofs is built from public Lean resources, large-scale proof synthesis, and agentic proving traces, containing 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized trajectories with retrieved context, failed attempts, feedback, and repairs. Across five benchmarks, OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.

David Ma, Kaijing Ma, Shawn Guo +7

M-A-P

Theorem Proving Formalization Unified Framework

Ask PDF