# Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions

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

## Key facts

- Cited by 22 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 33 references that are in the map.
- First posted on arXiv 17 Feb 2025.

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

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [NumGLUE: A Suite of Fundamental yet Challenging Mathematical Reasoning Tasks](https://mlsanity.com/paper/2204.05660/) (2022)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement](https://mlsanity.com/paper/2402.00745/) (2024)
- [A Symbolic Framework for Evaluating Mathematical Reasoning and Generalisation with Transformers](https://mlsanity.com/paper/2305.12563/) (2023)
- [Neural Machine Translation for Mathematical Formulae](https://mlsanity.com/paper/2305.16433/) (2023)
- [A Survey of Languages for Formalizing Mathematics](https://mlsanity.com/paper/2005.12876/) (2020)

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

- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition](https://mlsanity.com/paper/2510.06774/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [MASA: LLM-Driven Multi-Agent Systems for Autoformalization](https://mlsanity.com/paper/2510.08988/) (2025)
- [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](https://mlsanity.com/paper/2608.10916/) (2026)
- [The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning](https://mlsanity.com/paper/2603.15914/) (2026)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation](https://mlsanity.com/paper/2606.12594/) (2026)
- [Theory-Scale Auto-Formalization of Logics for Computer Science](https://mlsanity.com/paper/2606.26525/) (2026)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)
- [Do We Need Frontier Models to Verify Mathematical Proofs?](https://mlsanity.com/paper/2604.02450/) (2026)
- [COMPOSE: Composing Future Theorems from Citations and Formal Structure](https://mlsanity.com/paper/2605.30333/) (2026)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [The Knowledge-Reasoning Dissociation: Fundamental Limitations of LLMs in Clinical Natural Language Inference](https://mlsanity.com/paper/2508.10777/) (2025)
- [Monotonic Reference-Free Refinement for Autoformalization](https://mlsanity.com/paper/2601.23166/) (2026)
- [Mathematical Reasoning in Large Language Models: Benchmarks, Architectures, Evaluation, and Open Challenges](https://mlsanity.com/paper/2605.19723/) (2026)
- [MioFFAn: an Annotation Software for Formula Formalization with LLM Automation Capabilities](https://mlsanity.com/paper/2607.22552/) (2026)
- [Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation](https://mlsanity.com/paper/2608.17177/) (2026)
- [Definition Grounding in Theory-Level Auto-formalization](https://mlsanity.com/paper/2610.19223/) (2026)
- [Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization](https://mlsanity.com/paper/2610.20573/) (2026)

## Abstract (arXiv)

Thanks to their linguistic capabilities, LLMs offer an opportunity to bridge the gap between informal mathematics and formal languages through autoformalization. However, it is still unclear how well LLMs generalize to sophisticated and naturally occurring mathematical statements. To address this gap, we investigate the task of autoformalizing real-world mathematical definitions: a critical component of mathematical discourse. Specifically, we introduce two novel resources for autoformalization, collecting definitions from Wikipedia (Def_Wiki) and arXiv papers (Def_ArXiv). We then systematically evaluate a range of LLMs, analyzing their ability to formalize definitions into Isabelle/HOL. Furthermore, we investigate strategies to enhance LLMs' performance including refinement through external feedback from Proof Assistants, and formal definition grounding, where we augment LLMs' formalizations through relevant contextual elements from formal mathematical libraries. Our findings reveal that definitions present a greater challenge compared to existing benchmarks, such as miniF2F. In particular, we found that LLMs still struggle with self-correction, and aligning with relevant mathematical libraries. At the same time, structured refinement methods and definition grounding strategies yield notable improvements of up to 16% on self-correction capabilities and 43% on the reduction of undefined errors, highlighting promising directions for enhancing LLM-based autoformalization in real-world scenarios.