# MathAtlas: A Benchmark for Autoformalization in the Wild

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 33 references that are in the map.
- First posted on arXiv 13 May 2026.

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

- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Improving Text Embeddings with Large Language Models](https://mlsanity.com/paper/2401.00368/) (2023)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [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)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Towards a Mathematics Formalisation Assistant using Large Language Models](https://mlsanity.com/paper/2211.07524/) (2022)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)

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

- [Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning](https://mlsanity.com/paper/2605.28365/) (2026)
- [StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean](https://mlsanity.com/paper/2609.09264/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)
- [Definition Grounding in Theory-Level Auto-formalization](https://mlsanity.com/paper/2610.19223/) (2026)

## Abstract (arXiv)

Current autoformalization benchmarks are largely focused on olympiad or undergraduate mathematics, while graduate and research-level mathematics remains underexplored. In this paper, we introduce MathAtlas, the first large-scale autoformalization benchmark of in the wild graduate-level mathematics, containing ~52k theorems, definitions, exercises, examples, and proofs extracted from 103 graduate mathematics textbooks. MathAtlas is enriched with a mathematical dependency graph containing ~178k relations, and is the first autoformalization benchmark to include such relations, facilitating evaluation and development of dependency-aware autoformalization systems. Our extensive experiments show that MathAtlas is high quality but extremely challenging: strong baselines achieve at most 9.8% correctness on theorem statements and 16.7% on definitions. Furthermore, we find performance of state-of-the-art models degrades substantially with dependency depth: on MA-Hard, a subset of 700 entities with the deepest dependency trees, the best model achieves only 2.6% correctness for autoformalization on this challenging dataset. We release MathAtlas to the community as a benchmark set for large-scale autoformalization of graduate-level mathematics in the wild.