# Lean Pool: An AI-Maintained Archive of Formalized Mathematics

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 31 of its 231 references that are in the map.
- First posted on arXiv 21 Sep 2026.

## Builds on (most cited first, 30 of 31)

- [QJL: 1-Bit Quantized JL Transform for KV Cache Quantization with Zero Overhead](https://mlsanity.com/paper/2406.03482/) (2024)
- [First Proof](https://mlsanity.com/paper/2602.05192/) (2026)
- [Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization](https://mlsanity.com/paper/2606.31002/) (2026)
- [Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium](https://mlsanity.com/paper/2603.15929/) (2026)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)
- [VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean](https://mlsanity.com/paper/2602.18307/) (2026)
- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)
- [Learning to Repair Lean Proofs from Compiler Feedback](https://mlsanity.com/paper/2602.02990/) (2026)
- [A Domain Theory for Statistical Probabilistic Programming](https://mlsanity.com/paper/1811.04196/) (2018)
- [Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance](https://mlsanity.com/paper/2606.14000/) (2026)
- [TheoremGraph: Bridging Formal and Informal Mathematics](https://mlsanity.com/paper/2606.25363/) (2026)
- [An Evaluation of the Archive of Formal Proofs](https://mlsanity.com/paper/2104.01052/) (2021)
- [Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization](https://mlsanity.com/paper/2606.13925/) (2026)
- [Evaluation of LLMs for Mathematical Formalization in Lean](https://mlsanity.com/paper/2606.05632/) (2026)
- [Does My Embedding Reflect That A = B? Evaluating Mathematical Equivalence in Embedding Models](https://mlsanity.com/paper/2606.23959/) (2026)
- [A complete formalization of Fermat's Last Theorem for regular primes in Lean](https://mlsanity.com/paper/2410.01466/) (2024)
- [Optimal local linear convergence of Nesterov's accelerated gradient method for C2 functions under the Polyak--Lojasiewicz inequality](https://mlsanity.com/paper/2603.21516/) (2026)
- [Formalizing multi-graded Brenner-Schr"oer Proj schemes and dilatations of rings in Lean4](https://mlsanity.com/paper/2606.01438/) (2026)
- [A Formalization of the Mean-Field Derivation of the Vlasov Equation](https://mlsanity.com/paper/2607.08986/) (2026)
- [Vero: Can AI Agents Build Formally Verified Software Repositories?](https://mlsanity.com/paper/2608.13522/) (2026)
- [Formalizing computability theory via partial recursive functions](https://mlsanity.com/paper/1810.08380/) (2018)
- [A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics](https://mlsanity.com/paper/2201.10456/) (2022)
- [Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4](https://mlsanity.com/paper/2408.15180/) (2024)
- [Classifying the groups of order p q in Lean](https://mlsanity.com/paper/2501.09769/) (2025)
- [Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof](https://mlsanity.com/paper/2503.13276/) (2025)
- [2-Coloring Cycles in One Round](https://mlsanity.com/paper/2603.04235/) (2026)
- [A formal proof of the Ramanujan--Nagell theorem in Lean 4](https://mlsanity.com/paper/2604.09808/) (2026)
- [Maximizing Algebraic Connectivity with 2(n-2) Edges: The Large Vertex Number Case](https://mlsanity.com/paper/2608.07360/) (2026)
- [Dilatations of categories, via their lean formalization](https://mlsanity.com/paper/2608.09305/) (2026)
- [Completeness and incompleteness of basic matching logic](https://mlsanity.com/paper/2608.13306/) (2026)

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

- [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026)

## Abstract (arXiv)

Lean Pool is a repository of formalized mathematics. It is grown, maintained and optimized by AI agents.