At which level is it currently possible to write formal proofs?

Question

I am wondering whether I should try to have some fun using proof systems. I have never used such a system, but I have some experiences in logic and programming. My question is: At which level of abstraction is it currently possible to perform formal proofs using proof assistants with reasonable effort?

Of course many branches of contemporary research rely heavily on large and complex theories which fill books but have not been formalised at all. On the other hand there are theorems which are thousands of years old (irrationality of $\sqrt{2}$) whose proofs can be found in every example-page on the websites of the proof assistants. I would not find it very compelling to perform elementary proofs in say arithmetics, elementary number theory or euclidean geometry, I would prefer a context where there is already some more abstraction available. There must be some level in-between were it is still possible to perform proofs without having to formalise whole theories. How can we describe this level?

Let me give an illustrative example: We could try to prove existence and uniqueness of the Haar measure. It is an old theorem from 1940 and it only uses very established and common theories. The proof is technical and you would definitely have to do some hard work to get all inequalities right in a fully formalised version, but we might think—it is probably naive—that it would be a manageable project. However, if it turns out that there are not yet any definitions and theorems from measure theory in the proof assistant, if you would have to formalise some stuff about Banach spaces and some concrete function spaces first, and if even the available material for general topology is very limited, it might turn out to be a project taking years.

So, can anybody tell me what is already available and usable for reusage in proof assistants? Are there basic frameworks for say general topology and for dealing with the most common algebraic structures available which are usable and well-structured and not totally messed up and which are still maintained? With which kinds of structures can you actually work (measure spaces? categories? manifolds? function spaces?), this includes, of course, the most fundamental lemmata/theorems (since the community of formal proofs is not that big, of course I do not expect any of such collections to be as exhaustive as some informal, large books). Are there large differences between the major proof assistants (Isabelle, Coq, Mizar…) with respect to such support?

(I am not asking for the state of current big projects to formalise a theorem, for example by Hales, but I want to know where the software is “ready to use”)

Answer 1

One can possibly make some headway by switching from a traditional formulation of a field of mathematics to a "synthetic" formulation, where the objects under study are not explicitly built out of smaller pieces, but are universally characterized axiomatically. The historical prototype of such an approach is "synthetic differential geometry", where instead of defining what a smooth manifold is in the traditional way (which would take a lot of code), one imposes an axiom that guarantees that all objects/types under study behave like differentiable spaces with smooth functions between them.

Such synthetic formulations of traditional mathematics naturally lend themselves to axiomatization in proof management systems, specifically those based on type theory. Indeed, since intuitionistic type theory is precisely the internal logic of locally cartesian closed categories such as the smooth toposes of synthetic differential geometry, these are by design the systems that formalize synthetically formulated theories.

This gets even more pronounced as one passes from ordinary type theory to homotopy type theory, since here basic axioms are already so much more expressive. For instance where in ordinary type theory one formulates group theory in the traditional "piecewise" form, in homotopy type theory one finds that group theory is already built in, right out of the box: in an $\infty$-topos $\mathbf{H}$ group objects are equivalent to pointed connected objects $\mathbf{B}G$, and the slice $\infty$-topos $Act(G) \simeq \mathbf{H}_{/\mathbf{B}G}$ over such is the $\infty$-category of infinity-group actions. In homotopy type theory this means that a dependent type over a pointed connected type $\mathbf{B}G$ is a group representation (even an $\infty$-group representation up to coherent homotopy), dependent sum now is forming the induced representation, dependent product the co-induced representation. This yields a synthetic formulation of group theory and representation theory in homotopy type theory without adding a single extra axiom.

This option hasn't been explored much yet, as far as I can see, for doing formalized proofs. But I think it would be possible and worthwhile to do so.

One is therefore naturally led to wonder if one can usefully combine the synthetic description of differential geometry and that of higher gauge theory, aka higher group representation theory to find a synthetic formulation of modern higher differential geometry, that would naturally express modern concepts such as differential cohomology, D-module theory, étale stacks and the like. I have been exploring this a little under the name differential cohesive homotopy type theory where all this naturally exists, synthetically. Myself, I am not coding computer managed proofs myself, but for many of the statements that one proves in differential cohesive infinity-toposes it is or would be fairly straightforward to do so. Once on the n-Category Café we went through some basic exercises in this context and for instance proved in Coq from the axioms the long exact sequences that characterize differential cohomology, see here.

For more details, with Mike Shulman we have written an introduction to the synthetic axiomatization of higher differential geometry and higher gauge theory in homotopy type theory:

• Urs Schreiber, Mike Shulman, Quantum gauge field theory in cohesive homotopy type theory

Two weeks ago at the meeting of the Canadian Mathematical Society I advertized this approach further, see

• Urs Schreiber, Synthetic Quantum Field Theory

Answer 2

There are two threads of current development in proof systems: foundational and coverage. The foundational work tries to find the best meta-theory to formalize mathematics. Out of that work first came dependent types (AUTOMATH, in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions (current Coq). Currently a new wave of such work is being done in homotopy type theory as another step in this direction. Coq's library is not that large, except of course in the area of group theory where the results of the work on Feit-Thompson has produce something larger.

The much larger work has happened for decades building Mizar's enormous library [Note that Mizar is based on Tarski-Grothendieck set theory rather than type theory. Its library is a couple of orders of magnitude larger than anyone else's. Also worth a close look is NuPRL, HOL light and Isabelle, which all have decently sized libraries.

A rather thorough list of math systems has been collected by Freek Wiedijk.

Personally, I must admit that for the sheer joy of playing with mathematics, I rather like to use Agda. Unfortunately, its current library is fairly small, but the community is growing it quite quickly. For developing the kinds of mathematics I am currently interested in, it works quite well.

This whole area is the domain currently called mechanized mathematics -- there is an annual conference on that topic, with this (2013) year's instalment happening in early July in Bath.

Bottom line: none of these pieces of software are at the level of ease-of-use of say Maple or Mathematica, although some of them are probably close to SAGE. But they are evolving very quickly. They are way past the innovator stage, firmly into early adopter territory and growing.

Answer 3

Since this question has popped up again, I think someone should mention Kevin Buzzard's talk at the 2022 ICM, “The rise of formalism in mathematics”, available here on YouTube (slides here along an opinionated summary by Gil Kalai), in which he gives his answer to this thread's question by giving a number of examples of proofs formalized with the help of proof assistants (mostly Lean), or in the process of being thus formalized (sometimes very near completion), illustrating the fact that this works across a wide variety of fields, and both with “complex proofs” and with “complex objects”.