# APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries

arXiv: https://arxiv.org/abs/2504.19110 · HTML: https://mlsanity.com/paper/2504.19110/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 14 references that are in the map.
- First posted on arXiv 27 Apr 2025.

## Builds on (most cited first, 6 of 6)

- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [QED at Large: A Survey of Engineering of Formally Verified Software](https://mlsanity.com/paper/2003.06458/) (2020)
- [Proof Repair across Type Equivalences](https://mlsanity.com/paper/2010.00774/) (2020)

## Built on by (most cited first, 7 of 7)

- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Uncovering Hidden Correctness in LLM Causal Reasoning via Symbolic Verification](https://mlsanity.com/paper/2601.21210/) (2026)
- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment](https://mlsanity.com/paper/2507.08665/) (2025)
- [ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers](https://mlsanity.com/paper/2607.19407/) (2026)
- [ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib](https://mlsanity.com/paper/2608.20432/) (2026)
- [Definition Grounding in Theory-Level Auto-formalization](https://mlsanity.com/paper/2610.19223/) (2026)

## Abstract (arXiv)

While frontier formal mathematics systems now routinely develop repository-scale proof engineering artifacts requiring multi-file coordination and semantic correctness beyond compilation, existing evaluation benchmarks remain focused on isolated theorem proving. We introduce Automated Proof Engineering (APE), the first systematic framework for evaluating repository-scale proof engineering through dual verification that validates both syntactic compilation and semantic requirement satisfaction in pinned library environments. We present a complete infrastructure comprising APE-Bench, which automatically extracts proof engineering tasks from real library commit histories, and APE-Harness, a unified execution framework based on task contract abstraction. This contract-based design enables standardized evaluation across diverse formal mathematics tasks and fair systematic comparison of different agent implementations (including our APE-Agent reference scaffold alongside Claude Code and Codex CLI) on identical task specifications. We demonstrate the framework's effectiveness through comprehensive evaluation. All code and benchmark dataset are released as open-source at https://github.com/xinhjBrant/APE-Bench.