# AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness arXiv: https://arxiv.org/abs/2610.05367 ยท HTML: https://mlsanity.com/paper/2610.05367/ ## Key facts - No citing papers in the map yet (data through 14 Oct 2026). - Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. - Builds on 54 of its 88 references that are in the map. - First posted on arXiv 4 Oct 2026. ## Placed in - LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/) ## Builds on (most cited first, 30 of 54) - [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022) - [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017) - [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021) - [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024) - [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025) - [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022) - [Representation Learning with Contrastive Predictive Coding](https://mlsanity.com/paper/1807.03748/) (2018) - [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025) - [Gemma 3 Technical Report](https://mlsanity.com/paper/2503.19786/) (2025) - [gpt-oss-120b & gpt-oss-20b Model Card](https://mlsanity.com/paper/2508.10925/) (2025) - [Understanding R1-Zero-Like Training: A Critical Perspective](https://mlsanity.com/paper/2503.20783/) (2025) - [LIMA: Less Is More for Alignment](https://mlsanity.com/paper/2305.11206/) (2023) - [DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligence](https://mlsanity.com/paper/2606.19348/) (2026) - [Quantifying Language Models' Sensitivity to Spurious Features in Prompt Design or: How I learned to start worrying about prompt formatting](https://mlsanity.com/paper/2310.11324/) (2023) - [DeepSeek-V3.2: Pushing the Frontier of Open Large Language Models](https://mlsanity.com/paper/2512.02556/) (2025) - [GEPA: Reflective Prompt Evolution Can Outperform Reinforcement Learning](https://mlsanity.com/paper/2507.19457/) (2025) - [Cognitive Behaviors that Enable Self-Improving Reasoners, or, Four Habits of Highly Effective STaRs](https://mlsanity.com/paper/2503.01307/) (2025) - [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022) - [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025) - [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022) - [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024) - [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023) - [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025) - [RL's Razor: Why Online Reinforcement Learning Forgets Less](https://mlsanity.com/paper/2509.04259/) (2025) - [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024) - [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025) - [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019) - [OctoThinker: Mid-training Incentivizes Reinforcement Learning Scaling](https://mlsanity.com/paper/2506.20512/) (2025) - [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025) - [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026) ## Abstract (arXiv) 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.