# Towards a Mathematics Formalisation Assistant using Large Language Models

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

## Key facts

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

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

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [InCoder: A Generative Model for Code Infilling and Synthesis](https://mlsanity.com/paper/2204.05999/) (2022)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Jigsaw: Large Language Models meet Program Synthesis](https://mlsanity.com/paper/2112.02969/) (2021)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [A Survey on Semantic Parsing](https://mlsanity.com/paper/1812.00978/) (2018)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)

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

- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [A New Approach Towards Autoformalization](https://mlsanity.com/paper/2310.07957/) (2023)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification](https://mlsanity.com/paper/2504.17017/) (2025)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [Identifying, Evaluating, and Mitigating Risks of AI Thought Partnerships](https://mlsanity.com/paper/2505.16899/) (2025)
- [IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch](https://mlsanity.com/paper/2512.00997/) (2025)
- [Translating Informal Proofs into Formal Proofs Using a Chain of States](https://mlsanity.com/paper/2512.10317/) (2025)
- [Flow-based Extremal Mathematical Structure Discovery](https://mlsanity.com/paper/2601.18005/) (2026)
- [When Giant Language Brains Just Aren't Enough! Domain Pizzazz with Knowledge Sparkle Dust](https://mlsanity.com/paper/2305.07230/) (2023)
- [Pipeline for Verifying LLM-Generated Mathematical Solutions](https://mlsanity.com/paper/2602.20770/) (2026)
- [Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees](https://mlsanity.com/paper/2604.19000/) (2026)
- [A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs](https://mlsanity.com/paper/2609.10579/) (2026)

## Abstract (arXiv)

Mathematics formalisation is the task of writing mathematics (i.e., definitions, theorem statements, proofs) in natural language, as found in books and papers, into a formal language that can then be checked for correctness by a program. It is a thriving activity today, however formalisation remains cumbersome. In this paper, we explore the abilities of a large language model (Codex) to help with formalisation in the Lean theorem prover. We find that with careful input-dependent prompt selection and postprocessing, Codex is able to formalise short mathematical statements at undergrad level with nearly 75% accuracy for 120 theorem statements. For proofs quantitative analysis is infeasible and we undertake a detailed case study. We choose a diverse set of 13 theorems at undergrad level with proofs that fit in two-three paragraphs. We show that with a new prompting strategy Codex can formalise these proofs in natural language with at least one out of twelve Codex completion being easy to repair into a complete proof. This is surprising as essentially no aligned data exists for formalised mathematics, particularly for proofs. These results suggest that large language models are a promising avenue towards fully or partially automating formalisation.