mlsanityData to 7 Oct 2026

Towards a Mathematics Formalisation Assistant using Large Language Models

arXiv 2211.07524 ↗First posted 14 Nov 2022cs.CL cs.AIcited by 22

Not on the map. Why?

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.

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

Builds on

17 of 26 references.

References · 17

  1. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  2. 2020Language Models are Few-Shot Learnerscited by 32,199
  3. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  4. 2019Sentence-BERT: Sentence Embeddings using Siamese BERT-Networkscited by 9,049
  5. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,601
  6. 2022Competition-Level Code Generation with AlphaCodecited by 1,427
  7. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  8. 2022InCoder: A Generative Model for Code Infilling and Synthesiscited by 492
  9. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  10. 2022Autoformalization with Large Language Modelscited by 252
  11. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  12. 2021Jigsaw: Large Language Models meet Program Synthesiscited by 103
5 more
  1. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  2. 2018A Survey on Semantic Parsingcited by 62
  3. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 52
  4. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  5. 2022Formal Specifications from Natural Languagecited by 33

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 2; 2024: 6; 2025: 9; 2026: 5.

22 papers.

Sort:

By area:

  1. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  3. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 54
  4. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalizationcited by 53
  5. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  6. 2024Autoformalizing Euclidean Geometrycited by 27
  7. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  8. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
  9. 2023A New Approach Towards Autoformalizationcited by 10
  10. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 9
  11. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  12. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 9
10 more
  1. 2025Neural Theorem Proving: Generating and Structuring Proofs for Formal Verificationcited by 4
  2. 2025Identifying, Evaluating, and Mitigating Risks of AI Thought Partnershipscited by 3
  3. 2025IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touchcited by 3
  4. 2025Translating Informal Proofs into Formal Proofs Using a Chain of Statescited by 3
  5. 2026Flow-based Extremal Mathematical Structure Discoverycited by 3
  6. 2026MathAtlas: A Benchmark for Autoformalization in the Wildcited by 2
  7. 2023When Giant Language Brains Just Aren't Enough! Domain Pizzazz with Knowledge Sparkle Dustcited by 1
  8. 2026Pipeline for Verifying LLM-Generated Mathematical Solutionscited by 1
  9. 2026Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Treescited by 1
  10. 2026A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCscited by 0