Abstraction boundaries and spec driven development in pure mathematics
HTML articles powered by AMS MathViewer
- by Johan Commelin and Adam Topaz;
- Bull. Amer. Math. Soc. 61 (2024), 241-255
- DOI: https://doi.org/10.1090/bull/1831
- Published electronically: February 15, 2024
Abstract:
In this article we discuss how abstraction boundaries can help tame complexity in mathematical research with the help of an interactive theorem prover. While many of the ideas we present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.References
- Clark Barwick and Peter Haine, Pyknotic objects, I. Basic notions, Preprint, arXiv:1904.09966, (2019).
- Dustin Clausen and Peter Scholze, Condensed Mathematics and Complex Geometry, (2022), https://people.mpim-bonn.mpg.de/scholze/Complex.pdf.
- The Mathlib Community, The Lean mathematical library, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New York, NY, USA), CPP 2020, Association for Computing Machinery, 2020, pp. 367–381.
- The Mathlib Community, Completion of the Liquid Tensor Experiment, Blog Post, 2022, https://leanprover-community.github.io/blog/posts/lte-final/.
- Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer, The lean theorem prover (system description), Automated deduction—CADE 25, Lecture Notes in Comput. Sci., vol. 9195, Springer, Cham, 2015, pp. 378–388. MR 3446905, DOI 10.1007/978-3-319-21401-6_{2}6
- 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
- P. R. Halmos, How to write mathematics, Enseign. Math. (2) 16 (1970), 123–152. MR 277319
- G. W. Bond, Eulogy: Donald E. Knuth, Bull. London Math. Soc. 21 (1989), no. 1, 110–112 (Latin). With an English paraphrase. MR 967799, DOI 10.1112/blms/21.1.110
- Patrick Massot, Git Repository, https://github.com/PatrickMassot/leanblueprint.
- Peter Scholze, Lecture notes on Condensed Mathematics, (2019), https://www.math.uni-bonn.de/people/scholze/Condensed.pdf.
- Peter Scholze, Lectures on Analytic Geometry, (2019), https://www.math.uni-bonn.de/people/scholze/Analytic.pdf.
- Peter Scholze, Half a year of the Liquid Tensor Experiment: Amazing developments, Blog Post, 2021, https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/.
- Peter Scholze, Nonconvexity and discretization, MathOverflow, 2021, https://mathoverflow.net/q/386796.
- Peter Scholze, Liquid tensor experiment, Exp. Math. 31 (2022), no. 2, 349–354. MR 4458116, DOI 10.1080/10586458.2021.1926016
- Jean-Pierre Serre, How to write mathematics badly, 2007, https://www.youtube.com/watch?v=ECQyFzzBHlo.
- Adam Topaz, Definitions in the liquid tensor experiment, Blog Post, 2022, https://leanprover-community.github.io/blog/posts/lte-examples/.
- Hassler Whitney, Geometric integration theory, Princeton University Press, Princeton, NJ, 1957. MR 87148, DOI 10.1515/9781400877577
Bibliographic Information
- Johan Commelin
- Affiliation: Mathematisch Institut, Utrecht University, Budapestlaan 6, 3584CD Utrecht, Nederland
- MR Author ID: 1198615
- Email: j.m.commelin@uu.nl
- Adam Topaz
- Affiliation: Department of Mathematical and Statistical Sciences, University of Alberta, 632 Central Academic Building, Edmonton AB T6G 2G1, Canada
- MR Author ID: 1051144
- Email: topaz@ualberta.ca
- Received by editor(s): July 31, 2023
- Published electronically: February 15, 2024
- Additional Notes: The first author was supported by the Deutsche Forschungsgemeinschaft (DFG) grant CO 2587/1-1.
The second author was supported by NSERC discovery grant RGPIN-2019-04762. - © Copyright 2024 by the authors
- Journal: Bull. Amer. Math. Soc. 61 (2024), 241-255
- MSC (2020): Primary 68V30, 68V20, 00A35
- DOI: https://doi.org/10.1090/bull/1831
- MathSciNet review: 4726990