AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
cs.LO, cs.AI, cs.LG
Submitted: 2026-10-04
Updated: 2026-10-04
Code: https://github.com/oOo0oOo/lean-lsp-mcp
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Sources
- Aristotle: IMO-level Automated Theorem Proving
- gpt-oss-120b & gpt-oss-20b Model Card
- GEPA: Reflective Prompt Evolution Can Outperform Reinforcement Learning
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
- CSLib: The Lean Computer Science Library
- Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
- FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
- DeepSeek-V3.2: Pushing the Frontier of Open Large Language Models
- DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligence
- Gemma 3 Technical Report
- DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning
- SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
- Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
- Position: Agentic Evolution is the Path to Evolving LLMs
- Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization
- LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
- MiniMax-M1: Scaling Test-Time Compute Efficiently with Lightning Attention
- Formalizing Mathematics at Scale
- DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
- Proximal Policy Optimization Algorithms
Related papers
- Formalizing Flag Algebras in Lean
- An Information-Flow Perspective on Explainability Requirements: Specification and Verification
- A programming language combining quantum and classical control
- Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
- ADVENT: LLM-Driven Automatic Predicate Invention for ILP
- Encoder-Decoder Transformers: Logical Characterizations and Periodicity