Mathematical reasoning and the computer

Buzzard, Kevin

doi:10.1090/bull/1833

Mathematical reasoning and the computer
HTML articles powered by AMS MathViewer

by Kevin Buzzard

Bull. Amer. Math. Soc. 61 (2024), 211-224

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

Published electronically: February 15, 2024

HTML | PDF

Abstract:

Computers have already changed the way that humans do mathematics: they enable us to compute efficiently. But will they soon be helping us to reason? And will they one day start reasoning themselves? We give an overview of recent developments in neural networks, computer theorem provers, and large language models.

References

Laura Alessandretti, Andrea Baronchelli, and Yang-Hui He, Machine learning meets number theory: the data science of Birch-Swinnerton-Dyer, Machine learning in pure mathematics and theoretical physics, World Sci. Publ., Hackensack, NJ, [2023] ©2023, pp. 1–39. MR 4619158, DOI 10.1142/9781800613706_{0}001
Charles Blundell, Lars Buesing, Alex Davies, Petar Veličković, and Geordie Williamson, Towards combinatorial invariance for Kazhdan-Lusztig polynomials, Represent. Theory 26 (2022), 1145–1191. MR 4510816, DOI 10.1090/ert/624
Thomas F. Bloom, On a density conjecture about unit fractions, Preprint, arXiv:2112.03726, (2021).
Thomas F. Bloom and Bhavik Mehta, Unit fractions, https://b-mehta.github.io/unit-fractions/, April 24, 2023.
Johan Commelin, Liquid tensor experiment, Nieuw Arch. Wiskd. (5) 22 (2021), no. 4, 231–234 (Dutch, with Dutch summary). MR 4477665
Johan Commelin and Adam Topaz, Abstraction boundaries and spec driven development in pure mathematics, Bull. Amer. Math. Soc. (N.S.), (61) 2024, no. 2, ISSN: 0273-9079.
Bernd I. Dahn, Robbins algebras are Boolean: a revision of McCune’s computer-generated solution of Robbins problem, J. Algebra 208 (1998), no. 2, 526–532. MR 1655464, DOI 10.1006/jabr.1998.7467
Ernest Davis, Deep learning and mathematical intuition: A review of (Davies et al. 2021), arXiv:2112.04324, (2021).
Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis, Formalizing the solution to the cap set problem, 10th International Conference on Interactive Theorem Proving, LIPIcs. Leibniz Int. Proc. Inform., vol. 141, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2019, pp. Art. No. 15, 19. MR 4008934
Alex Davies, András Juhász, Marc Lackenby, and Nenad Tomasev, The signature and cusp geometry of hyperbolic knots, Preprint, arXiv:2111.15323, (2022).
Jordan S. Ellenberg and Dion Gijswijt, On large subsets of $\Bbb F^n_q$ with no three-term arithmetic progression, Ann. of Math. (2) 185 (2017), no. 1, 339–343. MR 3583358, DOI 10.4007/annals.2017.185.1.8
Siddhartha Gadgil, Formalizing Gardam’s disproof of Kaplansky’s unit conjecture, https://siddhartha-gadgil.github.io/automating-mathematics/posts/formalizing-gardam-disproof-kaplansky-conjecture/, April 24, 2023.
Giles Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. (2) 194 (2021), no. 3, 967–979. MR 4334981, DOI 10.4007/annals.2021.194.3.9
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, 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
Yang-Hui He, The Calabi-Yau landscape—from geometry, to physics, to machine learning, Lecture Notes in Mathematics, vol. 2293, Springer, Cham, [2021] ©2021. MR 4301304, DOI 10.1007/978-3-030-77562-9
Marc Lackenby, Using machine learning to formulate mathematical conjectures, https://www.youtube.com/watch?v=0ekP5M7w3dQ, April 24, 2023.
Adrien-Marie Legendre, Essai sur la théorie des nombres, Cambridge Library Collection, Cambridge University Press, Cambridge, 2009 (French). Reprint of the second (1808) edition. MR 2859036, DOI 10.1017/CBO9780511693199
Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet, Hypertree proof search for neural theorem proving, Advances in Neural Information Processing Systems (S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, eds.), vol. 35, Curran Associates, Inc., 2022, pp. 26337–26349.
The LMFDB Collaboration, The L-functions and modular forms database, https://www.lmfdb.org, 2023, April 24, 2023.
Allen Mann, A complete proof of the Robbins conjecture, http://math.colgate.edu/~amann/MA/robbins_complete.pdf, April 24, 2023.
Patrick Massot, Formal mathematics for mathematicians and mathematics students, https://www.youtube.com/watch?v=tp_h3vzkObo, April 24, 2023.
Patrick Massot, Floris van Doorn, and Oliver Nash, Formalising the $h$-principle and sphere eversion, CPP 2023: Proceeding of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 2023, pp. 121–134.
John Napier, The construction of the wonderful canon of logarithms, W. Blackwood and sons, 1889.
OpenAI, Chatgpt, https://chat.openai.com, April 24, 2023.
OpenAI, Gpt-4 technical report, 2023.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever, Formal mathematics statement curriculum learning, 2022.
J. D. Phillips and David Stanovský, Bruck loops with abelian inner mapping groups, Comm. Algebra 40 (2012), no. 7, 2449–2454. MR 2948838, DOI 10.1080/00927872.2011.579587
Peter Scholze, Liquid tensor experiment, Exp. Math. 31 (2022), no. 2, 349–354. MR 4458116, DOI 10.1080/10586458.2021.1926016
The Stacks Project Authors, Stacks Project, https://stacks.math.columbia.edu, 2018.
Adam Wagner, Finding counterexamples to conjectures via reinforcement learning, https://www.youtube.com/watch?v=vMLVH6IEwlM, April 24, 2023.
Adam Zsolt Wagner, Constructions in combinatorics via neural networks, 2021.