Towards a Mathematics Formalisation Assistant using Large Language Models
Abstract
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 theorem statements. For proofs quantitative analysis is infeasible and we undertake a detailed case study. We choose a diverse set of 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.
Keywords
Cite
@article{arxiv.2211.07524,
title = {Towards a Mathematics Formalisation Assistant using Large Language Models},
author = {Ayush Agrawal and Siddhartha Gadgil and Navin Goyal and Ashvni Narayanan and Anand Tadipatri},
journal= {arXiv preprint arXiv:2211.07524},
year = {2022}
}