Proof in the time of machines

Granville, Andrew

doi:10.1090/bull/1826

Proof in the time of machines
HTML articles powered by AMS MathViewer

by Andrew Granville;

Bull. Amer. Math. Soc. 61 (2024), 317-329

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

Published electronically: February 15, 2024

HTML | PDF | Request permission

Abstract:

We are concerned here with the nature of proof and what proof will become in this age of machines. We do so by comparing the values associated with (traditional) community based proof verification to those associated with computer proof verification. We finish by proposing ways that computer proofs might incorporate successful strategies from human experiences.

References

Kevin Buzzard, The Xena Project, a blog at https://xenaproject.wordpress.com/
Eugenia Cheng, Mathematics, morally, 2004 (preprint).
Alex Davies, Peter Veličković, Geordie Williamson, et al., Advancing mathematics by guiding human intuition with AI, Nature 600 (2021), 70–74.
Silvia De Toffoli, Reconciling Rigor and intuition, Erkenntnis 86 (2021), no. 6, 1783–1802. MR 4331052, DOI 10.1007/s10670-020-00280-x
Silvia De Toffoli, Groundwork for a fallibilist account of mathematics, The Philosophical Quarterly 71 (2021), 823–844.
M. Ganesalingam and W. T. Gowers, A fully automatic theorem prover with human-style output, J. Automat. Reason. 58 (2017), no. 2, 253–291. MR 3600894, DOI 10.1007/s10817-016-9377-1
Kurt Gödel, The modern development of the foundations of mathematics in the light of philosophy, draft of a 1961 presentation to the American Philosophical Society, Collected Works, Vol III, Oxford (1995), 375–388.
Andrew Granville, Accepted proofs: Objective truth, or culturally robust?, Annals of Math. and Philosophy 2 (2023), 66 pgs.
Donna Haraway, Situated knowledges: The science question in feminism and the privilege of partial perspective, Feminist studies, 14 (1988), 575–599.
Thomas S. Kuhn, The Structure of Scientific Revolutions (2nd ed), Chicago, University of Chicago Press, 1962.
Patrick Massot, Formal mathematics for mathematicians and mathematics students lecture on youtube.com (https://youtu.be/tp\underbar{ }h3vzkObo).
Melanie Mitchell, Artificial Intelligence: A Guide for Thinking Humans, Farrar, Straus and Giroux, 2019.
Rodrigo Ochigame, Automated mathematics and the reconfiguration of proof and labor, Bull. Amer. Math. Soc. (N.S.), (61) 2024, no. 3, ISSN: 0273-0979.
Julian Reiss and Jan Sprenger, Scientific Objectivity, The Stanford Encyclopedia of Philosophy (Winter 2020 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/cgi-bin/encyclopedia/archinfo.cgi?entry=scientific-objectivity
Michael Shulman, Strange new universes: Proof assistants and synthetic foundations, Bull. Amer. Math. Soc. (N.S.), (61) 2024, no. 2, ISSN: 0273-9079.
E. Szemerédi, On sets of integers containing no $k$ elements in arithmetic progression, Acta Arith. 27 (1975), 199–245. MR 369312, DOI 10.4064/aa-27-1-199-245
A. M. Turing, Computing machinery and intelligence, Mind 59 (1950), 433–460. MR 37064, DOI 10.1093/mind/LIX.236.433
Akshay Venkatesh, How we place value in mathematics, Bull. Amer. Math. Soc. (N.S.), (61) 2024, no. 2, ISSN: 0273-9079.
Avi Wigderson and Yuval Wigderson, The uncertainty principle: variations on a theme, Bull. Amer. Math. Soc. (N.S.) 58 (2021), no. 2, 225–261. MR 4229152, DOI 10.1090/bull/1715