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

Pseudo-Formalization for Automatic Proof Verification
May 19, 2026Slim Barkallah, Luke Bailey, Kaiyue Wen +2Proof Formalization
Stanford University
Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
Jun 30, 2026Arshia Soltani Moakhar, Iman Gholami, Max Springer +2Autoformalization Theorem Proving
OProver: A Unified Framework for Agentic Formal Theorem Proving
May 17, 2026David Ma, Kaijing Ma, Shawn Guo +7Theorem Proving Formalization
M-A-P

May 19, 2026, cs.LOJ/K move · Enter open · S save

Pseudo-Formalization for Automatic Proof Verification

Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid+1

Stanford University

Proof Formalization

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

Pseudo-Formalization for Automatic Proof Verification

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

OProver: A Unified Framework for Agentic Formal Theorem Proving