Mathematics and the formal turn

This paper discusses how mathematics can be represented in formal axiomatic systems with precise grammars and rules. The ability to represent mathematical definitions and proofs in formal systems is a striking contribution of modern logic. Building on these foundations, computational proof assistants make it possible to encode mathematical knowledge in digital form. The paper explores some ways these technologies can help us do mathematics.

Key innovations mentioned:
1. Verifying Theorems: Proof assistants can verify the correctness of mathematical proofs. Notable examples include the verification of Thomas Hales's proof of the Kepler conjecture and the Liquid Tensor Experiment.
2. Correcting Mistakes: Formal verification helps discover and correct errors in mathematical literature, as demonstrated by the formalization of the Kepler conjecture and Sébastien Gouëzel's work.
3. Gaining Insight: Formalization often leads to new insights. Examples include George Gonthier's characterization of planarity in terms of a hypermap and Scholze's realization about the computation of Ext-groups in the Liquid Tensor Experiment.
4. Building Libraries: The development of formal mathematical libraries, such as those of Mizar, Isabelle, HOL Light, Coq, Metamath, and Lean, leads to standardization of definitions and notation.
5. Searching for Definitions and Theorems: Technology like contemporary sledgehammer technology is beginning to help us find definitions and theorems. Large language models can also assist with formal oversight.
6. Refactoring Proofs: Digital formats allow mathematics to be searched, analyzed, and manipulated. Proof assistants enable users to tinker with and improve their mathematics.
7. Refactoring Libraries: Communities of formalizers often revise and refine fundamental concepts, with proof assistants helping to see the effects on downstream results.
8. Engineering Concepts: Refactoring formal libraries and proofs yields insights, such as using filters for the concept of a limit and embeddings between structures.
9. Communicating: New modes of communication have emerged around formal technologies, with mailing lists and social media platforms fostering collaboration.
10. Collaborating: Digital platforms support collaborative efforts, as demonstrated by the Liquid Tensor Experiment and formalization of the sphere eversion theorem.
11. Managing Complexity: Digital technology helps manage complexity by modularizing mathematical data and providing clear interfaces.
12. Managing the Literature: Conventional mathematical texts empower authors, but formal libraries put the reader in control by reducing definitions and proofs to axiomatic primitives.
13. Teaching: Interactive proof assistants provide quick feedback and help students recognize logical forms and keep track of objects and assumptions.
14. Improving Access: Formal technology makes mathematics more like writing computer programs, potentially improving access to a broader audience.
15. Using Mathematical Computation: Formal methods can make the use of symbolic and numeric computation more reliable.
16. Using Automated Reasoning: Automated reasoning tools, including first-order theorem provers, SAT solvers, SMT solvers, and term rewriters, can be used in mathematics.
17. Using Machine Learning: Machine learning can decide which theorems in a large formal library to use with a sledgehammer, and large language models can draft formal proof outlines.
18. Supporting a Synthesis of Machine Learning and Symbolic AI: Formal methods provide a platform for the synthesis of machine learning and symbolic reasoning, potentially leading to benefits beyond mathematics itself.

Main prior ingredients:
* Zermelo's axiomatization of set theory
* Russell and Whitehead's system of ramified type theory
* Automated reasoning tools
* Interactive proof assistants
* Formal axiomatic systems