Strange new universes: Proof assistants and synthetic foundations

Shulman, Michael

doi:10.1090/bull/1830

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