2022/11/14 by Ayush Agrawal, Agrawal, Ayush, Siddhartha Gadgil +8 · 7 citations
Computer Science · Mathematics · #Artificial intelligence #Automated theorem proving #Calculus (dental) #Computer science #Correctness #Language of mathematics #Mathematical proof #Mathematics #Mathematics education #Mathematics, Computing, and Information Processing #Natural Language Processing Techniques #Natural language #Programming language #Proof assistant #Semantic Web and Ontologies #Set (abstract data type) #Task (project management) #Theoretical computer science #Thriving #cs.AI #cs.CL
paper · pdf · doi:10.48550/arxiv.2211.07524
published in arXiv (Cornell University) (Cornell University)
arxiv created 2022/11/14 · openalex publication_date 2022/11/14 · arxiv updated 2022/11/15 · openalex created_date 2022/11/23 · openalex updated_date 2026/08/05
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.