Mathematics and the formal turn

Avigad, Jeremy

doi:10.1090/bull/1832

Mathematics and the formal turn
HTML articles powered by AMS MathViewer

by Jeremy Avigad;

Bull. Amer. Math. Soc. 61 (2024), 225-240

DOI: https://doi.org/10.1090/bull/1832

Published electronically: February 15, 2024

HTML | PDF | Request permission

Abstract:

Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems with precise grammars and rules of use. Building on such foundations, computational proof assistants now make it possible to encode mathematical knowledge in digital form. This article enumerates some of the ways that these and related technologies can help us do mathematics.

References

Jeremy Avigad, The mechanization of mathematics, Notices Amer. Math. Soc. 65 (2018), no. 6, 681–690. MR 3792862
Jeremy Avigad, Modularity in mathematics, Rev. Symb. Log. 13 (2020), no. 1, 47–79. MR 4079161, DOI 10.1017/s1755020317000387
Jeremy Avigad and John Harrison, Formally verified mathematics, Commun. ACM 57 (2014), no. 4, 66–75.
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio, A formalization of Dedekind domains and class groups of global fields, J. Automat. Reason. 66 (2022), no. 4, 611–637. MR 4505023, DOI 10.1007/s10817-022-09644-0
Alexander Bentkamp, Ramon Fernández Mir, and Jeremy Avigad, Verified reductions for optimization, Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2023 (Sriram Sankaranarayanan and Natasha Sharygina, eds.), Springer, 2023, pp. 74–92.
Joshua Brakensiek, Marijn Heule, John Mackey, and David Narváez, The resolution of Keller’s conjecture, Automated reasoning. Part I, Lecture Notes in Comput. Sci., vol. 12166, Springer, Cham, [2020] ©2020, pp. 48–65. MR 4139804
Kevin Buzzard, Proving theorems with computers, Notices Amer. Math. Soc. 67 (2020), no. 11, 1791–1799. MR 4201922, DOI 10.1090/noti
Davide Castelvecchi, Mathematicians welcome computer-assisted proof in “grand unification” theory, Nature 595 (2021), 18–19.
Joshua Clune, A formalized reduction of Keller’s conjecture, Conference on Certified Programs and Proofs (CPP) 2023 (Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic, eds.), ACM, 2023, pp. 90–101.
Henry Cohn, Abhinav Kumar, Stephen D. Miller, Danylo Radchenko, and Maryna Viazovska, The sphere packing problem in dimension 24, Ann. of Math. (2) 185 (2017), no. 3, 1017–1033. MR 3664817, DOI 10.4007/annals.2017.185.3.8
Alex Davies, Petar Velickovic, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomasev, Richard Tanburn, Peter W. Battaglia, Charles Blundell, András Juhász, Marc Lackenby, Geordie Williamson, Demis Hassabis, and Pushmeet Kohli, Advancing mathematics by guiding human intuition with AI, Nat. 600 (2021), no. 7887, 70–74.
Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel, Seventeen provers under the hammer, 13th International Conference on Interactive Theorem Proving, LIPIcs. Leibniz Int. Proc. Inform., vol. 237, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2022, pp. Art. No. 8, 18. MR 4481869, DOI 10.4230/lipics.itp.2022.8
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban, The Isabelle ENIGMA, 13th International Conference on Interactive Theorem Proving, LIPIcs. Leibniz Int. Proc. Inform., vol. 237, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2022, pp. Art. No. 16, 21. MR 4481877, DOI 10.4230/lipics.itp.2022.16
Georges Gonthier, Formal proof—the four-color theorem, Notices Amer. Math. Soc. 55 (2008), no. 11, 1382–1393. MR 2463991
Sébastien Gouëzel and Vladimir Shchur, Corrigendum: A corrected quantitative version of the Morse lemma [ MR3003738], J. Funct. Anal. 277 (2019), no. 4, 1258–1268. MR 3959731, DOI 10.1016/j.jfa.2019.02.021
Jerrold W. Grossman, Patterns of research in mathematics, Notices Amer. Math. Soc. 52 (2005), no. 1, 35–41. MR 2105568
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
Thomas C. Hales, A proof of the Kepler conjecture, Ann. of Math. (2) 162 (2005), no. 3, 1065–1185. MR 2179728, DOI 10.4007/annals.2005.162.1065
Thomas C. Hales, Dense sphere packings, London Mathematical Society Lecture Note Series, vol. 400, Cambridge University Press, Cambridge, 2012. A blueprint for formal proofs. MR 3012355, DOI 10.1017/CBO9781139193894
Thomas C. Hales, Mathematics in the age of the Turing machine, Turing’s legacy: developments from Turing’s ideas in logic, Lect. Notes Log., vol. 42, Assoc. Symbol. Logic, La Jolla, CA, 2014, pp. 253–298. MR 3497663
Thomas C. Hales, Developments in formal proofs, Astérisque 367-368 (2015), Exp. No. 1086, x, 387–410. MR 3363597
Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller, A revision of the proof of the Kepler conjecture, Discrete Comput. Geom. 44 (2010), no. 1, 1–34. MR 2639816, DOI 10.1007/s00454-009-9148-4
John Harrison, Verifying nonlinear real formulas via sums of squares, Theorem proving in higher order logics, Lecture Notes in Comput. Sci., vol. 4732, Springer, Berlin, 2007, pp. 102–118. MR 2550881, DOI 10.1007/978-3-540-74591-4_{9}
John Harrison, Josef Urban, and Freek Wiedijk, History of interactive theorem proving, Computational logic, Handb. Hist. Log., vol. 9, Elsevier/North-Holland, Amsterdam, 2014, pp. 135–214. MR 3362157, DOI 10.1016/B978-0-444-51624-4.50004-6
John Haugeland, Artificial intelligence: The very idea, MIT Press, 1985.
Harald Helfgott, The ternary Goldbach conjecture, Gac. R. Soc. Mat. Esp. 16 (2013), no. 4, 709–726 (Spanish). MR 3183798
Marijn J. H. Heule and Oliver Kullmann, The science of brute force, Commun. ACM 60 (2017), no. 8, 70–79.
Johannes Hölzl, Fabian Immler, and Brian Huffman, Type classes and filters for mathematical analysis in Isabelle/HOL, Interactive theorem proving, Lecture Notes in Comput. Sci., vol. 7998, Springer, Heidelberg, 2013, pp. 279–294. MR 3111278, DOI 10.1007/978-3-642-39634-2_{2}1
Fabian Immler, A verified ODE solver and the Lorenz attractor, J. Automat. Reason. 61 (2018), no. 1-4, 73–111. MR 3806498, DOI 10.1007/s10817-017-9448-y
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, CoRR abs/2210.12283 (2022).
M. Kerjean, F. Le Roux, P. Massot, M. Mayero, Z. Mesnil, S. Modeste, J. Narboux, and P. Rousselin, Utilisation des assistants de preuves pour l’enseignement en l1 retours d’expériences, La Gazette de le Société Mathématique de France (2022), no. 174.
Samantha Koretsky (ed.), Artificial intelligence to assist mathematical reasoning: Proceedings of a workshop, National Academies Press, Washington, DC, 2023.
Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote, Formally verified approximations of definite integrals, J. Automat. Reason. 62 (2019), no. 2, 281–300. MR 3910117, DOI 10.1007/s10817-018-9463-7
Assia Mahboubi and Thomas Sibut-Pinote, A formal proof of the irrationality of $\zeta (3)$, Log. Methods Comput. Sci. 17 (2021), no. 1, Paper No. 16, 25. MR 4219699
The mathlib Community, The Lean mathematical library, Certified Programs and Proofs (CPP) 2020 (Jasmin Blanchette and Catalin Hritcu, eds.), ACM, 2020, pp. 367–381.
Maciej Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kucinski, Piotr Milos, and Yuhuai Wu, Magnushammer: A transformer-based approach to premise selection, CoRR abs/2303.04488 (2023).
Loic Pottier, Connecting Gröbner bases programs with Coq to do proofs in algebra, geometry and arithmetics, Knowledge Exchange: Automated Provers and Proof Assistants (Piotr Rudnicki, Geoff Sutcliffe, Boris Konev, Renate A. Schmidt, and Stephan Schulz, eds.), CEUR Workshop Proceedings, vol. 418, CEUR-WS.org, 2008.
Justin Reich, Failure to disrupt: Why technology alone can’t transform education, Harvard University Press, Cambridge, MA, 2020.
Serge Richard and Qiwen Sun, Bibliometric analysis on mathematics, 3 snapshots: 2005, 2010, 2015, CoRR abs/2102.06831 (2021).
A. M. Turing, Computing machinery and intelligence, Mind 59 (1950), 433–460. MR 37064, DOI 10.1093/mind/LIX.236.433
Floris van Doorn, Patrick Massot, and Oliver Nash, Formalising the h-principle and sphere eversion, Certified Programs and Proofs (CPP) 2023 (Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic, eds.), ACM, 2023, pp. 121–134.
Adam Zsolt Wagner, Constructions in combinatorics via neural networks, CoRR abs/2104.14516 (2021).