39
$\begingroup$

There are many different proof assistants out there, and I think it is reasonable to expect that more or less all results we prove in everyday mathematics can be proven in any of them. One nice way to see it is the page Formalizing 100 Theorems, on which you can see that most theorems are proven in at least 5 different assistants. However, for some theorems, they have only been formalized in just one or two assistants.

What I was curious about is: are there any structural reasons for preferring some proof assistants to others when dealing with specific areas of mathematics? For instance, I notice that Isabelle appears to be the prevalent one for theorems in analysis present in the list (e.g. it is the only one in which Green's theorem has been formalized).

Now, I understand that some of the reasons behind this come from who is using the given assistant, and some self-perpetuating trends. For example, as far as I can see, a lot of Lean users have joined their community thanks to influence of Kevin Buzzard, an algebraic geometer, and a lot of work has been put into various projects of more algebraic nature.

Let me emphasize that the question I have does not regard such questions, but rather ones tied more directly to the way the proof assistants work. This post by Kevin Buzzard which discusses why (in his opinion) Lean is preferable for "proper maths", and I'd be interested in similar discussion for e.g. theorems in analysis.

$\endgroup$
0

2 Answers 2

49
$\begingroup$

I think that to a large extent this is an open problem, and I think that one reason it's still open is that not enough people are working on it. I would love to see some change here but right now I think the answer is "the community doesn't actually know".

It seems that there is evidence that certain parts of mathematics are more suited to certain axiomatic frameworks. I've heard Paulson also express this view. For example, as you note, Isabelle/HOL, which uses simple type theory, is currently the leader in late 19th and early 20th century analysis. If you want to do computations of homotopy groups of synthetic types then perhaps you want a homotopy type theory based prover. And so on and so on.

For me as an algebraic number theorist this is a problematic state of affairs, because number theory is like a parasite. Number theory has existed for 2500 years and when other areas come along it tries to incorporate them and figure out how to use them to make progress in number theory (we use analysis, algebra, combinatorics, geometry and topology, and even model theory, and everything is done using classical logic). Hence if you want to do modern number theory in one theorem prover, you have to be able to do essentially all of pure mathematics, in classical logic, in that one prover. Even something old hat like the proof of Fermat's Last Theorem uses a lot of analysis and geometry to prove a result in number theory. As has already been noted, one of the reasons that I have been strongly advocating for monolithic classical libraries like Lean's mathlib is precisely because I see it as the only viable solution for attacking research level number theory. The fact that mathlib has been used by Commelin et al to prove a theorem of Clausen and Scholze is evidence that this strategy works.

OK now let me get technical.

Historically, it seems to me that mathematicians tend over time to demand more from their foundations. Simple type theory is absolutely fine for doing classical analysis up to and including early 20th century results; work of Eberl formalising most of a text on classical analytic number theory is strong evidence for this. In Lean we are behind in analysis because we made some big decisions about doing everything in an extremely general way; for example it took a long time to prove the single-variable fundamental theorem of calculus because we insisted on setting up a huge framework of multivariable analysis and integrals taking values in Banach spaces first; had we just ploughed through an undergraduate text in real analysis we could have got there much more quickly, but that is not the mathlib style. I do suspect that in 5 years' time we will be way ahead of Isabelle/HOL in terms of classical analysis and analytic number theory, however I don't think that this has anything to do with axioms, I think that it has everything to do with momentum, and the communities involved; i.e., it will be true for sociological reasons, rather than reasons to do with axioms.

With the advent of abstract algebra in the 20th century, leading onto homological methods and then abstractions such as schemes, the concept of the dependent type came to the fore (a sheaf on a scheme is an example of a dependent type; the point is that this concept is structurally logically more complex than, for example, the Riemann zeta function). I challenged the HOL people to formalise the definition of a scheme, and Paulson et al rose to the challenge and formalised schemes in Isabelle/HOL. However they could not use the Isabelle/HOL ring theory library and had to rewrite the theory of rings from the ground up in a different way, because of limitations of the HOL logic. This did not happen in Lean; we just used Lean's rings to make Lean's schemes. Is the Lean theory of schemes usable? Yes -- people like mathematics undergraduate Andrew Yang and my PhD student Jujian Zhang and several others are slowly working through the basic MSc-level material in the theory; Yang for example defined the fibre product of two schemes recently, and Zhang defined projective schemes. Based on this I would now certainly conjecture that we can do anything in the Stacks project in Lean. But is all this possible to do in Isabelle/HOL? Well, (a) nobody knows and (b) as far as I know, nobody is trying to find out. This is the problem we face; the community is too small. Furthermore if a classical mathematician is interested in schemes and wants to try using a theorem prover, Lean would be a very natural choice for them, again simply because there is both momentum, and evidence that it's working. But does this prove that a workable theory of schemes cannot be defined in HOL or in a univalent theory? It most certainly does not. It just means nobody is trying.

Finite group theory is another interesting example. In Coq they have a full proof of the odd order theorem. I've heard many times from the computer science community the idea that it would be an interesting challenge to formalise the full proof of the classification of finite simple groups, with the justification being that it's a gigantic proof so it would be another benchmark, and that some mathematicians are uneasy about the proof because of its nature. On the other hand I've also heard mathematicians express the idea that this would be an absolutely terrible project to embark upon because who cares about tens of thousands of lemmas in finite group theory, when group theory was fashionable in the 70s and 80s but things have very much moved on since then; we have seen how much noise the Clausen-Scholze work has generated in the math community and the reason for this is that it was targetting mathematics which research mathematicians in 2022 care about, as opposed to mathematics which is now in some sense less mainstream. Again we see that there are sociological issues at stake. Would it be possible to formalise a proof of the classification of finite simple groups in Coq? Probably! Would it be possible to do it in essentially any system? Probably! Will anyone do it? Who knows; I am personally doubtful right now. It would cost so much in person-hours to type in the books into a theorem prover. Ask me again when Google have figured out how to make a machine which turns regular textbooks into formalised mathematics.

A final subtlety here is that sometimes statements which mathematicians write down have different interpretations in formal systems. For example the statement that $\pi_1(S^1)=\mathbb{Z}$ is a statement which people in univalent systems say they can prove in a few lines; however the $S^1$ they're talking about is a synthetic combinatorial $S^1$, and their $\pi_1$ is a combinatorial $\pi_1$. Of course one can prove on paper that the synthetic $\pi_1(S^1)$ is isomorphic to the topological $\pi_1$ of the topological $S^1$, but the point is that the true claim that univalent systems are good at computing fundamental groups of spheres cannot be generalised to the statement that they're good at computing fundamental groups of topological spaces, because there are plenty of topological spaces like Grassmannians which nobody knows how to define synthetically, so the methods fail.

I think that real manifolds are another very interesting test case. We have them in Lean, due to work of Gouezel and others, but this was hard won. We still (at the time of writing) are not able to do basic linear algebra with vector bundles on these manifolds, as far as I know (for example taking the tensor product of two vector bundles). Is this because of foundational issues, or is it just that we're not trying hard enough? We'll find out soon enough, I'm sure. Are other foundations better equipped to solve the problem of doing things like exterior powers of vector bundles on real manifolds? WE DON'T KNOW. Which is the best system for defining de Rham cohomology of a real manifold? WE DON'T KNOW. And we don't know because people are not working on this problem. It would not surprise me at all if somewhere in the proof of Fermat's Last Theorem we need the fact that the analytically defined de Rham cohomology of a smooth projective complex variety agrees with algebraic de Rham cohomology; this sort of stuff is crucial when trying to understand the etale cohomology of modular curves and more generally Shimura varieties in terms of automorphic forms. But nobody is thinking about this question in any prover other than Lean, and in Lean progress is slow.

Let me end then with a question which I think is terrifically important and which I would love to see progress on. Given that to do number theory you need to be able to do all of pure mathematics, is it possible to create a monolithic mathematics library in every standard theorem prover which covers all of, say, the undergraduate degree in the University of Cambridge? Note that when I went there in the late 80s we certainly covered de Rham cohomology and tensor products of vector bundles on manifolds (I make this comment to stop the usual crowd of computer scientists saying "oh surely we have an undergraduate mathematical degree by now" -- we absolutely do not and there will be a lot of work to do before we get there, at least if we're aiming for Cambridge standards). I think that if people start working on this question (which we are working hard on in Lean with mathlib and I would love to see some rivals to mathlib springing up powered by other provers with other logics -- remember that mathlib is only just over 4 years old) then, and only then, will we be able to start giving coherent answers to your questions. In particular, it's only once we actually start trying to do everything in all systems that we will begin to understand whether there are parts of mathematics which just are intrisically really hard to formalise in a usable way within certain logical frameworks.

My guess: post-1960s alegebraic geometry cannot be done in a usable way in a HOL system (of course it can be done, it's just that it might not be practical and usable). And I have absolutely no idea what can be done in a univalent system because the moment you start using a univalent system you seem to fall into some kind of univalent hole and only ever work on problems specific to univalence; this is perhaps why Voevodsky, who won a Fields Medal for proving theorems about schemes, never defined a scheme in a theorem prover, whereas in Lean a team consisting mostly of undergraduates knocked off a prototype in a few weeks (using classical reasoning; I think that this was a problem for Voevodsky). I don't see any reason why there can't be a Coq version of mathlib; again the reason it's not there is I suspect sociological rather than anything else. The point about making the library monolithic is that then you are not allowed to have more than one version of rings (or more than one version of the natural numbers; the last time I checked there were four or five variants available to Coq users) -- in a monolithic library you need a consistent collection of definitions all of which play well with each other. Once we are seeing progress like this, we'll be able to understand this question better.

$\endgroup$
3
  • $\begingroup$ Has condensed math really won prizes already? I thought it was more the point that Scholze thought it was more interesting than the stuff he won the prizes for. $\endgroup$
    – Will Sawin
    Feb 9 at 14:38
  • $\begingroup$ Thank you for this amazing answer! As I expected the answer to why differnt parts of math have different representation in different proof assistants mainly due to sociological reasons, but I appreciate you expounding the cases to date where different logics have shown different kinds of difficulties (and highlighting that in the future the picture might become more transparent). I'm also surprised at you calling Wiles's work "old hat", but given the amount of progress in the past decades which stemmed from it, I guess there is some merit to it :) $\endgroup$
    – Wojowu
    Feb 9 at 15:03
  • $\begingroup$ Thanks Will -- I edited. $\endgroup$ Feb 23 at 0:01
3
$\begingroup$

I don't think most theorem provers are very different from each other. In my opinion most provers are based around classical logic, intuitionistic logic or possibly linear logic.

Many theorem provers seem to loosely correspond to a Heyting algebra or maybe the category of sets or maybe some sort of topos. There are complicated technical reasons why this isn't really true. For example, you probably want functional and propositional extensionality. But a topos works as a loose approximation of extensional dependent type theory.

A major difference seems to be whether one works in a boolean topos (loosely speaking classical logic) or a more constructive logic. This allows you to consistently axiomize features incompatible with classical logic such as the Schanuel topos which I am personally interested in because it is supposed to handle variables in a nice way. IIRC rewrite rules for axioms that compute is still an open problem.

There are some proof assistants with different interpretations than some sort of topos.

I don't really understand homotopy type theory but IIRC they are aiming for some sort of interpretation in terms of infinity groupoids or more simply the topos of simplicial sets. They're basically aiming at figuring out what a "higher topos" ought to look like.

Substructural logics which often deal with resources are a more conventional example. Stuff like separation logic is often formalized from within an existing prover but some often specialized ones have a bit more direct support. The traditional semantic for linear logic are in terms of star autonomous categories or IIRC for linear dependent type theory you want a nicer sort of category indexed by a monoidal category.

Modal logic has an application to interpreting macros/staged programming.

In a way you can see formalization of languages which resemble the simply typed lambda calculus as a synthetic formalization of closed Cartesian categories.

These are the main cases I see and personally I think that's kind of sad. I think we should look at the internal languages of all kinds of categories.

I think there is no real reason why Set is a good place to do mathematics in and Set^op is not. Cointuitionistic logic is very very niche but has an interesting relationship with CABAs, nondeterminism, control flow and logic programming languages.

There are some theorem provers out there which seem to not have easy semantics in Set. IIRC MetaMath more directly relies on axiomizing everything and loosely you can build up whatever sort of framework you like. I'm not really sure what sort of categorical semantics tools like Twelf based on LF (Logical Framework) ought to have.

IIRC there was this one visual prover based on string diagrams and monoidal categories for doing higher category theory.

It still seems to me most proof assistants are based on classical logic, intuitionistic logic or linear logic.

I would greatly love to hear about counterexamples in the comments.

$\endgroup$
1
  • 1
    $\begingroup$ One of those visual proof assistants for higher categories is Globular $\endgroup$ May 17 at 16:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.