Document Type
Article
Publication Date
2-15-2024
Journal Title
Bulletin of the American Mathematical Society
Volume Number
61
Issue Number
2
First Page
257
Last Page
270
DOI
https://doi.org/10.1090/bull/1830
Version
Publisher PDF: the final published version of the article, with professional formatting and typesetting
Abstract
Existing computer programs called proof assistants can verify the correctness of mathematical proofs but their specialized proof languages present a barrier to entry for many mathematicians. Large language models have the potential to lower this barrier, enabling mathematicians to interact with proof assistants in a more familiar vernacular. Among other advantages, this may allow mathematicians to explore radically new kinds of mathematics using an LLM-powered proof assistant to train their intuitions as well as ensure their arguments are correct. Existing proof assistants have already played this role for fields such as homotopy type theory.
Digital USD Citation
Shulman, Michael, "Strange new universes: Proof assistants and synthetic foundations" (2024). Mathematics: Faculty Scholarship. 10.
https://digital.sandiego.edu/mathematics-faculty/10
