Pith. sign in

REVIEW 4 cited by

Towards a Mathematics Formalisation Assistant using Large Language Models

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2211.07524 v1 pith:T34L3TWQ submitted 2022-11-14 cs.CL cs.AI

Ayush Agrawal , Siddhartha Gadgil , Navin Goyal , Ashvni Narayanan , Anand Tadipatri This is my paper · ORCID
classification cs.CLcs.AI
keywords languageformalisationproofscodexmathematicslargestatementstheorem
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
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 $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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization

    cs.LG 2025-07 conditional novelty 6.0 of 10

    GTED uses tree edit distance on operator trees of standardized Lean statements to evaluate autoformalization, ranking top on miniF2F and joint-top on ProofNet.

  2. Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine

    cs.AI 2025-06 conditional novelty 6.0 of 10

    SDE-GPG samples from a knowledge-point-to-definition mapping table, runs the AlphaGeometry symbolic deduction engine to produce conclusions, filters candidates with a checking function, and translates the formal outpu...

  3. Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations

    cs.CL 2025-05 conditional novelty 5.0 of 10

    The proposed Faithful-Refiner, combining syntactic parsing, quantifier and consistency checks, logical-relation guidance, and detailed proof feedback, raises explanation refinement rates on three NLI benchmarks by lar...

  4. Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks

    cs.CL 2025-05 reject novelty 5.0 of 10

    A grammar-based model of LLM-generated SMT-LIB code produces uncertainty signals that predict formalization errors on some reasoning tasks, with fused signals giving large error reductions only in an in-sample evaluation.

Pith tools