Strange new universes: Proof assistants and synthetic foundations
HTML articles powered by AMS MathViewer
- by Michael Shulman
- Bull. Amer. Math. Soc. 61 (2024), 257-270
- DOI: https://doi.org/10.1090/bull/1830
- Published electronically: February 15, 2024
- HTML | PDF
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.References
- Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri, Towards a mathematics formalisation assistant using large language models, arXiv:2211.07524, 2022.
- Andrej Bauer, What makes dependent type theory more suitable than set theory for proof assistants? MathOverflow, 2020. https://mathoverflow.net/q/376973 (version: 2020-12-07).
- Kuen-Bang Hou, Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory, Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016), ACM, New York, 2016, pp. 10. MR 3776776, DOI 10.1145/2933575.2934545
- Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, and Lars Birkedal, Modalities and parametric adjoints, ACM Trans. Comput. Log. 23 (2022), no. 3, Art. 18, 29. MR 4461936, DOI 10.1145/3514241
- Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal, Multimodal dependent type theory, Log. Methods Comput. Sci. 17 (2021), no. 3, Paper No. 11, 67. MR 4298414, DOI 10.46298/lmcs-17(3:11)2021
- Georges Gonthier, Formal proof—the four-color theorem, Notices Amer. Math. Soc. 55 (2008), no. 11, 1382–1393. MR 2463991
- Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller, A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), e2, 29. MR 3659768, DOI 10.1017/fmp.2017.1
- Albert Jiang, Charles Edgar Staats, Christian Szegedy, Markus Rabe, Mateja Jamnik, Wenda Li, and Yuhuai Tony Wu, Autoformalization with large language models, In NeurIPS, 2022. To appear. arXiv:2205.12615.
- Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample, Draft, sketch, and prove: Guiding formal theorem provers with informal proofs, In ICLR, 2023. arXiv:2210.12283.
- Krzysztof Kapulkin and Peter LeFanu Lumsdaine, The simplicial model of univalent foundations (after Voevodsky), J. Eur. Math. Soc. (JEMS) 23 (2021), no. 6, 2071–2126. MR 4244523, DOI 10.4171/JEMS/1050
- F. William Lawvere, An elementary theory of the category of sets (long version) with commentary, Repr. Theory Appl. Categ. 11 (2005), 1–35. Reprinted and expanded from Proc. Nat. Acad. Sci. U.S.A. 52 (1964) [MR0172807]; With comments by the author and Colin McLarty. MR 2177727
- Daniel R. Licata and Michael Shulman, Calculating the fundamental group of the circle in homotopy type theory, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), IEEE Computer Soc., Los Alamitos, CA, 2013, pp. 223–232. MR 3323808, DOI 10.1109/LICS.2013.28
- Jacob Lurie, Higher topos theory, Annals of Mathematics Studies, vol. 170, Princeton University Press, Princeton, NJ, 2009. MR 2522659, DOI 10.1515/9781400830558
- Jacob Lurie, Higher algebra, Available at http://www.math.harvard.edu/~lurie/, Sep 2014.
- Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium ’73 (Bristol, 1973) Stud. Logic Found. Math., Vol. 80, North-Holland, Amsterdam-Oxford, 1975, pp. 73–118. MR 387009
- Per Martin-Löf, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, vol. 1, Bibliopolis, Naples, 1984. Notes by Giovanni Sambin. MR 769301
- Peter Scholze, Half a year of the liquid tensor experiment: Amazing developments, https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/, June 2021.
- Philipp Stassen, Daniel Gratzer, and Lars Birkedal, $\texttt {mitten}$: a flexible multimodal proof assistant, 28th International Conference on Types for Proofs and Programs, LIPIcs. Leibniz Int. Proc. Inform., vol. 269, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2023, pp. Art. No. 6, 23. MR 4627539, DOI 10.4230/lipics.types.2022.6
- Michael Shulman, A formal proof that $\pi _1(s^1)=\mathbb {Z}$, http://homotopytypetheory.org/2011/04/29/a-formal-proof-that-pi1s1-is-z/, 2011.
- Michael Shulman, Idempotents in intensional type theory, Log. Methods Comput. Sci. 12 (2016), no. 3, Paper No. 10, 24. MR 3548859, DOI 10.2168/lmcs-12(3:9)2016
- Michael Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Math. Structures Comput. Sci. 28 (2018), no. 6, 856–941. MR 3798599, DOI 10.1017/S0960129517000147
- Michael Shulman, All $(\infty ,1)$-toposes have strict univalent universes, arXiv:1904.07004, 2019.
- Michael Shulman, Why doesn’t mathematics collapse even though humans quite often make mistakes in their proofs? MathOverflow, 2020. https://mathoverflow.net/q/338620 (version: 2020-06-15).
- Michael Shulman, Semantics of multimodal adjoint type theory, Electronic Notes in Theoretical Informatics and Computer Science, vol. 3 Proceeding of MFPS XXXIX, arXiv:2303.02572, (2023).
- The Univalent Foundations Program, Homotopy type theory—univalent foundations of mathematics, The Univalent Foundations Program, Princeton, NJ; Institute for Advanced Study (IAS), Princeton, NJ, 2013. MR 3204653
Bibliographic Information
- Michael Shulman
- Affiliation: Department of Mathematics, University of San Diego, San Diego, California 92110
- MR Author ID: 830320
- ORCID: 0000-0002-9948-6682
- Email: shulman@sandiego.edu
- Received by editor(s): August 12, 2023
- Published electronically: February 15, 2024
- Additional Notes: This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009.
- © Copyright 2024 by Michael Shulman
- Journal: Bull. Amer. Math. Soc. 61 (2024), 257-270
- MSC (2020): Primary 68V20
- DOI: https://doi.org/10.1090/bull/1830
- MathSciNet review: 4726991