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.
Bibliographic Information
- Kevin Buzzard
- Affiliation: Department of Mathematics, Imperial College London, London SW7 2AZ, United Kingdom
- MR Author ID: 363443
- ORCID: 0000-0002-7187-5109
- Email: k.buzzard@imperial.ac.uk
- Received by editor(s): September 13, 2023
- Published electronically: February 15, 2024
- © Copyright 2024 by the author
- Journal: Bull. Amer. Math. Soc. 61 (2024), 211-224
- MSC (2020): Primary 68T01; Secondary 68T07, 68V15, 68V20
- DOI: https://doi.org/10.1090/bull/1833
- MathSciNet review: 4726988