Which proof assistant would you advise me to learn (in 2022) considering my interests?

Question

I am a math teacher in college. I’m very interested in type theory. So far, I got the general idea of it but I would like to go deeper. I am interested in philosophy of maths, in foundations of maths, in topos theory. I would like to understand the univalence axiom.

I think learning how to use a proof assistant could help me attain these goals. Of course, I’ll be also happy to know something new and which appears to be more and more important in maths.

Which proof assistant would you advise me to learn (in 2022) considering my interests?

Answer 1

There is no single right answer and all of this will be highly subjective. Before I get into the details based on the subjects you want to learn, I would just say, pick something, play around with it, and have fun. Just like learning programming languages, you can learn more than one, you can switch at any time, and knowing one makes it easier to learn others.

Let's break down the subjects you want to learn. For certain reasons I'm going to go in reverse order:

Univalence axiom

Homotopy Type Theory (HoTT) is based on dependent type theory (DTT), and if you are interested in doing HoTT, you will need to learn DTT. As with all of your topics you wish to learn, there is no particular need to learn DTT via a proof assistant. The first chapter of the HoTT book, has a great introduction on dependent type theory (and the book is a great introduction to HoTT). Having said that, it does make a lot of sense to learn dependent type theory with a proof assistant. The three most used DTT-based proof assistants are likely Lean, Coq, and Agda. Lean has a number of great learning resources and it has a large user base, but it won't be great for univalence per se since Lean doesn't support HoTT for technical and social reasons. Lean has mostly been used for formalizing classical mathematics.

Coq and Agda have stronger support for HoTT and libraries for doing proofs in HoTT. Both also have a number of learning resources and large communities. Also (hat tip to Mike), Martín Hötzel Escardó has a course Introduction to Univalent Foundations of Mathematics with Agda which teaches HoTT alongside Agda.

I also want to mention Cubical Type Theory (CuTT). This is a variation (or family of variations) of DTT with properties built into the type theory which make it possible to prove univalence directly instead of having it as an axiom. It is maybe less pure than DTT + Univalence, but it is maybe more practical to work with (citation needed).

For me, one other proof assistant stands out which also has direct built in support for some HoTT features, namely Arend (see comment by Mike). It is very much experimental. (I'm not really sure if anyone uses it for serious work.) But on the other hand it is quite professional with a good user interface. (It is a research project of a company which makes IDEs for programming languages, so it has a very clean user experience.) Moreover, it has a tutorial specifically focusing on learning Arend alongside learning HoTT.

(Also, I should mention even after you learn DTT, it still might make sense to learn HoTT from the HoTT book.)

Topos Theory

There are certainly some connections between proof assistants, type theory, and toposes. However, I personally found knowing a proof assistant didn't help an especially large amount in learning what a topos was, but that was me. To learn about toposes, you probably need to learn some category theory first. Category theory does have very strong connections to type theory, which a good category theory book should explore.

I'm still new to toposes, but here are a few observations that I think helps when learning about toposes having already learned about proof assistants.

In proof assistants you are working in a "world of mathematics". You can think of this world as being a sort of set theory where types are sets. But this is just one interpretation (and one that breaks down with HoTT). Topos theory describes what makes a "world of mathematics". Type theory is the internal logic for working in any topos. (More specifically intuitionist higher order logic is the internal logic of a elementary topos. There are other extensions of the definition of topos which capture the models of DTT, HoTT, etc.)

Another observation is that the main ingredient in the definition of a topos is what in Lean and Coq is called Prop, the type of truth values. (In classical logic, Prop is isomorphic to Bool which is the two element set {true, false}, but in constructive logic it has a richer structure.) In theorem provers, subsets (or subtypes) of a type A are just maps f: A -> Prop. In a topos theory, this Prop is often denoted $\Omega$ and is called a subobject classifier.

Foundations of mathematics

Foundations of mathematics can mean a lot of things to a lot of people. Proof assistants present a sort of practical foundations of mathematics, where one actually comes up with a usable set of rules and axioms for doing mathematics formally in practice. Mizar and Metamath (set.mm) use a set theory foundation which is more similar to how foundations is taught in a typical university logic course. HOL-Light, HOL4, and Isabelle/HOL use higher order logic, which is a simpler type theory. And as we already mentioned Lean, Coq, and Agda use dependent type theory.

This will look very different from what you would typically read in a typical foundations of mathematics text book, focused on first order logic, model theory, ZFC set theory, and the like. Besides using different foundations, these books typically explore the meta-mathematical properties of logic, e.g. Gödel's theorems, the constancy of ZF - AC, and properties of computability theory. Moreover, you often have to look to other books if you want to learn the meta-mathematics of type theory, such as cut elimination, strong normalization, models of type theory, etc.

You might find Logic and Proof interesting, which is an early course on foundations which also uses and teaches the Lean proof assistant at the same time. (Although this might be too elementary for you given your background, and you just might want to skim it for the parts which are novel to you.)

Philosophy of mathematics

The classical questions in philosophy of mathematics are questions about what are mathematical objects and how does mathematics relate to the real world. For that I recommend the book "Thinking about Mathematics: The Philosophy of Mathematics" by Steward Shapiro.

However, proof assistants open up a more "practical" set of philosophical questions. We have a theory of what mathematics and proofs are that is over 100 years old. In this theory, proofs are, formally, just lists of steps where each step follows from an axiom or deduction rule in some formal system like FOL+ZFC. However, there is a large disconnect between how mathematics is done in practice, and that foundational viewpoint. What is a proof "really" to a mathematician, and how can this be used to build better tools and automation to formalize mathematics? I'm extremely influenced by my advisor, Jeremy Avigad, on this line of thinking, for example in his recent article Varieties of mathematical understanding.

Answer 2

I really cannot improve on Jason Rute's answer, but one suggestion I would have: after playing around with whatever theorem prover you decided to use, dabble around with a few others.

In particular, Automath is useful to play with, since it introduced many concepts adopted by later proof assistants. And the literature on Automath is freely available online. Concepts like "book equality" vs "definitional equality", etc., were first introduced by Automath and are necessary to understand Homotopy Type Theory.

Answer 3

I can't (yet) recommend AutoMath, except for historical interest. But, I resurrected it here AutoMath (GitHub) on GitHub, with upgrade on its syntax.

Its biggest weakness, by far, is its inability to handle equational logic. That was the motivation for and selling point of Homotopy Type Theory. As you can see in some of the demo files in the GitHub, there's just way too much baggage needed to do even the simplest equational proofs, because it has no concept of equations; particularly: of embedding equations into contexts, e.g. if $a = b$ then $φ(a) = φ(b)$, where $φ(\_)$ denotes a generic context.

The second biggest weakness is what I also count as a weakness of all the higher-order type theories in common use: their tendency toward over-reductionism, conflating and even confusing things that should be kept distinct. Among other things, it conflates ∃ with ∧, and ∀ with ⊃, and sorts with propositions. For AutoMath, this manifests itself by the awkward way it handles universal quantifiers.