# Evaluation of LLMs for Mathematical Formalization in Lean

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 23 references that are in the map.
- First posted on arXiv 4 Jun 2026.

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Does Prompt Formatting Have Any Impact on LLM Performance?](https://mlsanity.com/paper/2411.10541/) (2024)
- [Multi-Agent Design: Optimizing Agents with Better Prompts and Topologies](https://mlsanity.com/paper/2502.02533/) (2025)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics](https://mlsanity.com/paper/2505.03171/) (2025)
- [DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning](https://mlsanity.com/paper/2505.23754/) (2025)
- [ICPC-Eval: Probing the Frontiers of LLM Reasoning with Competitive Programming Contests](https://mlsanity.com/paper/2506.04894/) (2025)
- [RLMEval: Evaluating Research-Level Neural Theorem Proving](https://mlsanity.com/paper/2510.25427/) (2025)
- [Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques](https://mlsanity.com/paper/2502.03321/) (2025)

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

- [Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization](https://mlsanity.com/paper/2606.13925/) (2026)
- [Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification](https://mlsanity.com/paper/2609.11319/) (2026)
- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)

## Abstract (arXiv)

Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@k and refine@k metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of <0.01 per correct proof.