Proofs for a price: Tomorrow’s ultra-rigorous mathematical culture

De Toffoli, Silvia

doi:10.1090/bull/1823

Proofs for a price: Tomorrow’s ultra-rigorous mathematical culture
HTML articles powered by AMS MathViewer

by Silvia De Toffoli;

Bull. Amer. Math. Soc. 61 (2024), 395-410

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

Published electronically: May 15, 2024

HTML | PDF | Request permission

Abstract:

Computational tools might tempt us to renounce complete certainty. By forgoing of rigorous proof, we could get (very) probable results for a fraction of the cost. But is it really true that proofs (as we know and love them) can lead us to certainty? Maybe not. Proofs do not wear their correctness on their sleeve, and we are not infallible in checking them. This suggests that we need help to check our results. When our fellow mathematicians will be too tired or too busy to scrutinize our putative proofs, computer proof assistants could help. But feeding a mathematical argument to a computer is hard. Still, we might be willing to undertake the endeavor in view of the extra perks that formalization may bring—chiefly among them, an enhanced mathematical understanding.

References

Jeremy Avigad, The mechanization of mathematics, Notices Amer. Math. Soc. 65 (2018), no. 6, 681–690. MR 3792862
Jeremy Avigad, Reliability of mathematical inference, Synthese 198 (2021), no. 8, 7377–7399. MR 4292724, DOI 10.1007/s11229-019-02524-y
Jeremy Avigad, Varieties of mathematical understanding, Bull. Amer. Math. Soc. (N.S.) 59 (2022), no. 1, 99–117. MR 4340829, DOI 10.1090/S0273-0979-2021-01726-5
John P. Burgess and Silvia De Toffoli, What is mathematical rigor?, Aphex 25 (2022), 1–17.
Kevin Buzzard, What is the point of computers? A question for pure mathematicians, Preprint, arXiv:2112.11598, (2021).
Roderick M. Chisholm, Theory of knowledge, Prentice-Hall, 1966.
Silvia De Toffoli, Groundwork for a fallibilist account of mathematics, The Philosophical Quarterly 71 (2021), no. 4, 823–844.
Silvia De Toffoli, Who’s afraid of mathematical diagrams?, Philosophers’ Imprint 23 (2023), no. 1, 1–20.
Catherine Elgin, Understanding and the facts, Philosophical Studies 132 (2007), no. 1, 33–42.
Alvin Goldman, A causal theory of knowing, Journal of Philosophy 64 (1967), no. 12, 357–372.
Alvin Goldman, What is justified belief?, George S. Pappas (ed.), pp. 1–23, D. Reidel Publishing Company, 1979.
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
Michael Harris, Mathematics without apologies, Princeton University Press, Princeton, NJ, 2015. Portrait of a problematic vocation. MR 3289987, DOI 10.1515/9781400852024
David Hilbert, Mathematical problems, Bull. Amer. Math. Soc. (N.S.) 37 (2000), no. 4, 407–436. Reprinted from Bull. Amer. Math. Soc. 8 (1902), 437–479. MR 1779412, DOI 10.1090/S0273-0979-00-00881-8
John Horgan, The last universal mathematician, Scientific American (1994), 33–34.
Leslie Lamport, How to write a 21st century proof, J. Fixed Point Theory Appl. 11 (2012), no. 1, 43–63. MR 2955006, DOI 10.1007/s11784-012-0071-6
Patrick Massot, Why formalize mathematics?, https://www.imo.universite-paris-saclay.fr/~patrick.massot/files/exposition/why_formalize.pdf, 2021.
Plato, Theaetetus, Hackett Publishing Company, 1992.
Bertrand Russell, Human Knowledge: Its Scope and Limits, New York: Taylor & Francis Routledge, 1st ed. 1948, (2009).
Peter Scholze, Lectures on analytic geometry, https://www.math.uni-bonn.de/people/scholze/Analytic.pdf, 2019.
William P. Thurston, On proof and progress in mathematics, Bull. Amer. Math. Soc. (N.S.) 30 (1994), no. 2, 161–177. MR 1249357, DOI 10.1090/S0273-0979-1994-00502-6
Akshay Venkatesh, Some thoughts on automation and mathematical research, Bull. Amer. Math. Soc. (N.S.) 61 (2024), no. 2, 203–210. MR 4726987, DOI 10.1090/bull/1834
Vladimir Voevodsky, The origins and motivations of univalent foundations, The Institute Letter (The Institute for Advanced Studies), (2014), https://www.ias.edu/ideas/2014/voevodsky-origins.
Doron Zeilberger, Theorems for a price: tomorrow’s semi-rigorous mathematical culture, Math. Intelligencer 16 (1994), no. 4, 11–14, 76. Reprinted from Notices Amer. Math. Soc. 40 (1993), no. 8, 978–981 [ MR1239765 (94i:00007)]. MR 1294994, DOI 10.1007/BF03024696