--- title: "Towards Autoformalization of Mathematics and Code" description: "Checking long mathematical proofs by hand is cognitively demanding. 1 reference, cited by 15 papers here." authors: ["Garett Cunningham", "Razvan Bunescu", "David Juedes"] year: 2022 venue: "Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP)" source: "https://aclanthology.org/2022.mathnlp-1.4/" doi: "10.18653/v1/2022.mathnlp-1.4" arxiv: "2301.02195" licence: "CC BY 4.0 (ACL Anthology)" licence_url: "https://creativecommons.org/licenses/by/4.0/" summary_licence: "Elamur Cosmic License" canonical: "https://research.elamur.ai/free/en/papers/cunningham-2022-autoformalization-mathematics-code-correctness-experiments/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/cunningham-2022-autoformalization-mathematics-code-correctness-experiments/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2022](https://md.research.elamur.ai/free/en/papers/2022/page/6/) / Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs # Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs **Authors:** Garett Cunningham, [Razvan Bunescu](https://md.research.elamur.ai/free/en/authors/razvan-bunescu/) and David Juedes · **Year:** 2022 · **Venue:** [Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP)](https://md.research.elamur.ai/free/en/venues/mathnlp/) ([MathNLP 2022](https://md.research.elamur.ai/free/en/venues/mathnlp/2022/)) · **Publisher:** [Association for Computational Linguistics](https://md.research.elamur.ai/free/en/publishers/association-for-computational-linguistics/) · **Licence:** [CC BY 4.0 (ACL Anthology)](https://creativecommons.org/licenses/by/4.0/) **Links:** [Publisher's page](https://aclanthology.org/2022.mathnlp-1.4/) · [PDF](https://aclanthology.org/2022.mathnlp-1.4.pdf) · [DOI 10.18653/v1/2022.mathnlp-1.4](https://doi.org/10.18653/v1/2022.mathnlp-1.4) · [arXiv 2301.02195](https://arxiv.org/abs/2301.02195) · [OpenAlex](https://openalex.org/W4385574125) **Citations:** 10 citations (OpenAlex, 2026-10-14) · [15](https://md.research.elamur.ai/free/en/papers/cunningham-2022-autoformalization-mathematics-code-correctness-experiments/cited-by/) in our library, of the 149,439 papers whose bibliographies we read ## Summary Checking long mathematical proofs by hand is cognitively demanding. Autoformalization aims to help by converting natural-language proofs into code that an interactive theorem prover can check. The authors frame this as semantic parsing: LaTeX theorem–proof pairs are mapped to Coq. They cover elementary arithmetic and, separately, the correctness of simple imperative programs annotated with Hoare triples. Training data is synthetic. A few hand-written seed examples guided the design of a rich grammar that produces LaTeX and Coq versions roughly in parallel. This includes features such as sublemmas, coreference, and different proof directions. The model is a Universal Transformer with relative positional encodings and a copying mechanism, which handles unseen numbers and variable names. Results are measured by exact token match and by a semantic check, in which Coq verifies the generated proof. The models generalize well to intermediate expression lengths and program sizes absent from training, but fail on lengths beyond the training range. They also handle hand-written inputs, though less accurately. The work suggests autoformalization is feasible in narrow domains, with possible uses in teaching proofs and software verification. ## Key points - **Datasets:** four classes of examples. EVEN-ODD, COMPOSITES and POWERS are arithmetic; POLY covers Hoare-logic code correctness. The grammars can in principle yield over 283 million arithmetic and over 491,000 code examples. - **Splits:** 5,000 EVEN-ODD, 5,000 COMPOSITES and 2,000 POWERS examples were generated for each of training and testing. Training used n ∈ {2, 3, 5, 7, 9}; testing covered n from 2 to 12. - **Handwritten test set:** an extra 45 human-written LaTeX pairs, 15 per arithmetic class, test robustness to grammatical structures outside the generator. - **Positional encodings:** with absolute positional encodings, a Transformer scored 0% sequence-level accuracy on unseen lengths, so relative encodings were essential. - **POLY model:** a deeper model (8 blocks, 8 recurrent passes, 8 heads) generalized to unseen program lengths of 4–10 lines, and depth clearly helped. Sequence-level and semantic-level accuracy coincided for POLY. Code and data are at github.com/gc974517/autoformalization. *Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.* ## Institutions - [University of North Carolina at Charlotte](https://md.research.elamur.ai/free/en/universities/university-of-north-carolina-at-charlotte/) — University, Charlotte, United States · 10 works · 553 citations - [Ohio University](https://md.research.elamur.ai/free/en/universities/ohio-university/) — University, Athens, United States · 3 works · 335 citations 📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,959 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,789 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works 🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works ## Cite Cite as: Garett Cunningham, Razvan Bunescu and David Juedes. 2022. Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs. Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP). The paper itself, not this page. BibTeX from the library's record of the work. ```bibtex @inproceedings{cunningham2022autoformalization, title = {{Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs}}, author = {Garett Cunningham, Razvan Bunescu and David Juedes}, booktitle = {Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP)}, year = {2022}, doi = {10.18653/v1/2022.mathnlp-1.4}, eprint = {2301.02195}, archivePrefix = {arXiv}, url = {https://doi.org/10.18653/v1/2022.mathnlp-1.4} } ``` - [← previous Low-Resource Authorship Style Transfer: Can Non-Famous Authors Be Imitated?](https://md.research.elamur.ai/free/en/papers/patel-2022-low-resource-authorship-style-transfer/) - [next → AraDepSu: Detecting Depression and Suicidal Ideation in Arabic Tweets Using Transformers](https://md.research.elamur.ai/free/en/papers/hassib-2022-aradepsu-detecting-depression-suicidal-ideation/) - [↑ back to papers of 2022](https://md.research.elamur.ai/free/en/papers/2022/page/6/) ## References 1 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet. 1. K. Appel and W. Haken. 1977. Every planar map is four colorable, part I: discharging. Illinois Journal of Mathematics, 21(3):429 – 490. \#\#\# 4.3 Handwritten Examples K. Appel, W. Haken, and J. Koch. 1977. Every planar map is four colorable. II: Reducibility. Ill. J. Math., 21:491–567. [find](https://scholar.google.com/scholar?q=K%2E+Appel+and+W%2E+Haken%2E+1977%2E+Every+planar+map+is+four+colorable%2C+part+I%3A+discharging%2E+Illinois+Journal+of+Mathematics%2C+21%283%29%3A429+%E2%80%93+490%2E+%5C%23%5C%23%5C%23+4%2E3+Handwritten+Examples+K%2E+Appel%2C+W%2E+Haken%2C+and+J%2E+Koch%2E) *Updated 3 November 2026*