Abstract
I analyse differences in style between traditional prose mathematics writing and computer-formalised mathematics writing, presenting five case studies. I note two aspects where good style seems to differ between the two: in their incorporation of computation and of abstraction. I argue that this reflects a different mathematical aesthetic for formalised mathematics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Examples include Agda, Coq, Lean, HOL Light, Isabelle, Metamath and Mizar.
- 2.
- 3.
Down from 117 vectors in the original Kochen–Specker proof. Following Peres’ notation, \(\bar{1}\) is shorthand for \(-1\), 2 is shorthand for \(\sqrt{2}\), and \(\bar{2}\) is shorthand for \(-\sqrt{2}\).
- 4.
- 5.
A second difference is that when running the greedy algorithm from a partial colouring produces a contradiction, the formalised version does not write out the certificate: an explicit path of deductions leading to the concluding contradiction. But this is less controversial. In the case of the configuration in Fig. 2, when the path of deductions is written out, it does not appear to contain any particular insight. See Harrison [17, section 3.4] for a similar example.
- 6.
Gonthier et al. [12, section 4.3] report a similar example, in which an appeal to a logical decision procedure produces an “intellectually more satisfying” proof than the original argument involving a detailed combinatorial case analysis.
- 7.
There is an alternative approach using trigonometric identities.
- 8.
Mathlib [8], RingTheory/Polynomial/Chebyshev, line 209.
- 9.
- 10.
We normalise indices before the computation.
- 11.
Indeed, let \(k+b\) be the chosen instantiation of the \((m+1)\)-inductive hypothesis and \(k+a\) that of the m-inductive hypothesis:
$$\begin{aligned} 2T_{m+1}T_{(m+1)+(k+b)}&=T_{2(m+1)+(k+b)}+T_{k+b},\\ 2T_mT_{m+(k+c)}&=T_{2m+(k+c)}+T_{k+c}. \end{aligned}$$In order for there to be a nontrivial polynomial relation among these, the goal
$$ 2T_{m+2}T_{(m+2)+k}=T_{2(m+2)+k}+T_{k}, $$and some uses of the recurrence, we need to arrange that the T-indices which appear,
$$ m+\{2,1,0\},\quad k+\{0,b, c\},\quad m+k+\{2, b+1, c\},\quad 2m+k+\{4, b+2, c\}, $$are all either (a) sets of three consecutive numbers (in which case the recurrence relation provides an identity connecting them) or (b) all the same. This forces \(c=2\), and that forces \(b=1\), leading to the instantiations \((\star _1)\), \((\star _2)\) chosen.
- 12.
Your reader has immediate access to a full exposition of an unfamiliar abstraction; moreover, thanks to verification, she can trust you when you state that all the preconditions hold for that abstraction to be applicable in the context at hand.
- 13.
- 14.
Mathlib [8], Topology/MetricSpace/Antilipschitz.
- 15.
Mathlib [8], Analysis/InnerProductSpace/LaxMilgram.
- 16.
To believe that habitual abstraction really will avoid the repetition of proofs at large scale, you must be something of a Platonist: you must believe (as I do!) that the “natural context” of an argument is sufficiently unambiguous that others who need it will formulate it in the same way, and thus be led to stumble across your version.
- 17.
Mathlib [8], Geometry/Manifold/ChartedSpace.
- 18.
Mathlib [8], Geometry/Manifold/ChartedSpace, line 139.
- 19.
Mathlib [8], Geometry/Manifold/VectorBundle/Basic, line 486.
- 20.
Mathlib [8], Geometry/Manifold/LocalInvariantProperties, line 698.
- 21.
A crude analogy is to consider the statements of a mathematical theory as a digraph, with edges denoting easy implications (some implications are easy in both directions and their edges are bidirectional). To design a mathematical theory development, you must select a spanning tree for this digraph.
References
Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Competing inheritance paths in dependent type theory: a case study in functional analysis. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 3–20. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_1
Arnold, V.I.: On teaching mathematics. Russ. Math. Surv. 53(1), 229–236 (1998). https://doi.org/10.1070/RM1998v053n01ABEH000005
Boldo, S., Clément, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax-Milgram theorem. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 79–89. Association for Computing Machinery, New York, NY, USA (2017). https://doi.org/10.1145/3018610.3018625
Bonsall, F.F.: A down-to-earth view of mathematics. Am. Math. Mon. 89(1), 8–15 (1982). https://doi.org/10.2307/2320989
Bourbaki, N.: The architecture of mathematics. Am. Math. Mon. 57(4), 221–232 (1950). https://doi.org/10.2307/2305937
Chaieb, A., Wenzel, M.: Context aware calculation and deduction. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM -2007. LNCS (LNAI), vol. 4573, pp. 27–39. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_3
Commelin, J., Topaz, A.: Abstraction boundaries and spec driven development in pure mathematics. Bull. Am. Math. Soc. 61(2), 241–255 (2024). https://doi.org/10.1090/bull/1831
mathlib community, T.: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367–381. Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3372885.3373824
Conway, J.H., Burgiel, H., Goodman-Strauss, C.: The Symmetries of Things, A K Peters, Wellesley, MA (2008). https://doi.org/10.1201/b21368
Eck, D.: Wallpaper symmetry sketchpad. https://math.hws.edu/eck/js/symmetry/wallpaper.html. Accessed 25 March 2024
Gonthier, G.: Formal proof - the four color theorem. Notices Am. Math. Soc. 55(11), 1382–1393 (2008). www.ams.org/notices/200811/tx081101382p.pdf
Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_14
Gouëzel, S.: A formalization of the change of variables formula for integrals in mathlib. In: Buzzard, K., Kutsia, T. (eds.) Intelligent Computer Mathematics: 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022, Proceedings, pp. 3–18. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-16681-5_1
Hales, T., et al.: A formal proof of the Kepler conjecture. Forum Math. Pi 5, e2 (2017). https://doi.org/10.1017/fmp.2017.1
Halmos, P.R.: How to write mathematics. Enseign. Math. 2(16), 123–152 (1970)
Hardy, G.H.: A mathematician’s apology. Cambridge University Press (1940)
Harrison, J.: Formalized mathematics. Technical Report 36, Turku Centre for Computer Science (TUCS), Lemminkäisenkatu 14 A, FIN-20520 Turku, Finland (1996). http://www.cl.cam.ac.uk/~jrh13/papers/form-math3.html
Harrison, J.: Automating elementary number-theoretic proofs using Gröbner bases. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 51–66. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_5
Harrison, J.: Formalizing an analytic proof of the prime number theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reason. 43, 243–261 (2009). https://doi.org/10.1007/s10817-009-9145-6
Howard, P.: Lecture notes for M612: Partial Differential Equations (2020). https://people.tamu.edu/~phoward/M612.html
Immler, F.: A verified ODE solver and the Lorenz attractor. J. Autom. Reason. 61(1), 73–111 (2018). https://doi.org/10.1007/s10817-017-9448-y
Inglis, M., Aberdein, A.: Beauty is not simplicity: an analysis of mathematicians’ proof appraisals. Philosophia Math. 23(1), 87–109 (07 2014). https://doi.org/10.1093/philmat/nku014
Kobayashi, S., Nomizu, K.: Foundations of Differential Geometry, Volume I, Issue 15, Volumes 1-2 of Interscience Tracts in Pure and Applied Mathematics, Interscience Publishers, New York, NY (1963)
Kochen, S., Specker, E.P.: The problem of hidden variables in quantum mechanics. J. Math. Mech. 17(1), 59–87 (1967)
Montaño, U.: Ugly mathematics: why do mathematicians dislike computer-assisted proofs? Math. Intell. 34(4), 21–28 (2012). https://doi.org/10.1007/s00283-012-9325-9
Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625–635. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_37
de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26
Peres, A.: Two simple proofs of the Kochen-Specker theorem. J. Phys. A Math. Gen. 24(4), l175–l178 (1991). https://doi.org/10.1088/0305-4470/24/4/003
Pottier, L.: Connecting Gröbner bases programs with Coq to do proofs in algebra, geometry and arithmetics. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008. CEUR Workshop Proceedings, vol. 418, CEUR-WS.org (2008). https://ceur-ws.org/Vol-418/paper5.pdf
Rota, G.C.: The phenomenology of mathematical beauty. Synthese 111(2), 171–182 (1997). https://doi.org/10.1023/A:1004930722234
Tao, T.: What is good mathematics? Bull. Am. Math. Soc. New Ser. 44(4), 623–634 (2007). https://doi.org/10.1090/S0273-0979-07-01168-8
Wells, D.: Are these the most beautiful? Math. Intell. 12(3), 37–41 (1990). https://doi.org/10.1007/BF03024015
Acknowledgements
I am grateful to Isabelle Petersen for assistance in typesetting the notes for this article. I also thank the audience of the first version of this material (a talk at the 2023 workshop “Machine Assisted Proof” at the Institute for Pure and Applied Mathematics), whose stimulating comments helped to sharpen the argument, and Tom Hales, John Harrison and Kim Morrison for useful comments on a draft.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Ethics declarations
Disclosure of Interests
The author has no competing interests to declare that are relevant to the content of this article.
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Macbeth, H. (2024). Algorithm and Abstraction in Formal Mathematics. In: Buzzard, K., Dickenstein, A., Eick, B., Leykin, A., Ren, Y. (eds) Mathematical Software – ICMS 2024. ICMS 2024. Lecture Notes in Computer Science, vol 14749. Springer, Cham. https://doi.org/10.1007/978-3-031-64529-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-031-64529-7_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-64528-0
Online ISBN: 978-3-031-64529-7
eBook Packages: Computer ScienceComputer Science (R0)