Why should mathematicians care about formalization?
Why Lean might be a better choice for mathematicians?
Quotes from CICM 2020 Slack chat log
Can we get one system which is capable of understanding all of the mathematics in my university's undergraduate pure maths degree?
Maybe the HoTT systems are best for cohomology theories, maybe the dependent type systems are best for algebraic geometry, maybe the simply typed systems are best for analysis...
But this is not good enough for modern mathematics. In modern number theory I need all of these things at the same time.
So we have to find one system or perhaps more generally one logical foundation which will do for everything.
I think that neither mathematicians nor AI people will be able to profitably use mathematics written in more than one system.
So I think we have to find the formal framework which works best for all of pure mathematics.
And if none of the current ones do then trying to formalise undergraduate maths in all of them will perhaps teach us about what kind of new frameworks will work.
-- Kevin Buzzard
I wrote a PhD thesis 25 years ago, which is a long time ago in mathematics standards. One could ask how close we are to formalising that thesis today. And the answer is that we are a million miles away.
I didn't do anything particularly complicated, like many maths PhD theses my results were mainly incremental. In fact one of the motivations that my advisor had for getting me to prove the results was that they were essentially already known by work of my advisor but my advisor's proof used work which he didn't understand and which not all of the community accepted.
Having used these theorem proving systems, I believe that eg my PhD work could in theory be formalised.
But it would take many thousands of person hours and who cares about it anyway? It's 25 years old.
This in my mind represents a big problem.
It is exactly the reason why many mathematicians see no point in these computer proof systems.
We have to start somewhere.
Mathematics doesn't build on top of all previous work, it builds on top of the important stuff.
By asking questions such as "can we formalise this recent paper -- even the statements of the results", we will I think be dragging formalisation towards the interests of research mathematicians who work in the areas where they give out the fields medals.
And it's the important people in these areas who are deciding where the funding is going.
We have to make the area look more like it is engaging with modern research mathematics in areas which the fields medal committee think is fashionable.
But we can't even begin to do this until we can do undergraduate mathematics.
I formalise because I am now old enough that I don't need to play the game any more.
So I have decided to work in an area which I believe is really important, rather than an area which is fashionable.
More precisely I have decided to work in an area whose importance will become clearer to mathematicians later on.
But formalising now is like typesetting was before LaTeX.
It's clunky, it's hard, it can be messy.
By attempting to drive it in the direction of modern mathematics I hope to begin to understand why it's difficult for mathematicians to use the current systems, and why it's difficult to formalise standard PhD level stuff.
I think that these questions are in some sense poorly understood because so little of this kind of mathematics is being done in theorem provers.
I think that formalising undergraduate mathematics in an arbitrary prover teaches you the limitations of your prover.
And whilst I totally understand that there are many provers and provers are used for many things.
I think that the question of which prover is best for all pure mathematics is not at all well understood.
But I think that the fields medal committee will not be remotely interested until we have a system which can begin to think about research level mathematics.
And the odd order proof is evidence that just getting really good (fields Medal level) at one area of mathematics (an area which is not fashionable any more) isn't good enough.
Modern mathematics borrows from many areas.
Number theory has been around for 2000 years and takes from all other areas. We use geometry, we use topology, we use category theory, we use analysis, we use algebra.
Isabelle-HOL is really good at analysis. The HoTT systems are really good at category theory. Lean is getting really good at algebra.
Hence none of them are ready for modern number theory.
Because you need one system which is really good at all of them.
I want a mechanical assistant who can help me to do modern number theory.
So I need to find out which system is the best.
I'm not asking that it proves new theorems for me, I'm asking that it can check calculations and do the boring part of the job where I check all the diagrams commute and the proofs in the literature which work under some assumptions also work in some slightly more general situation.
I think that we might be able to have these before I die.
But first we have to work out if the system we're going to use is one of the currently existing ones or whether we need a new one which can be built on what we have learnt by trying and failing to do mathematics in fields medal areas in the current systems.
I see huge potential for collaboration between mathematicians and computer scientists here.
But the mathematicians won't come until we convince them that we're ready, and I'm not sure that we are right now. We can't even understand some of the questions on some standard undergraduate exams right now, so we are clearly not ready.
On the other hand, making Lean ready is really good fun.
-- Kevin Buzzard
I think Lean has a really good user interface compared to most other systems. Isabelle is the only system that I would say has a similar level of polish and modernity in its UI.
But Isabelle/HOL has a weak type system and this is a deal breaker for some.
I think that over-focus on constructivity has been cited as a significant minus of Coq from the point of view of traditional mathematicians getting into formalization.
this being an entirely social phenomenon that separates Coq and Lean despite their having near-identical foundations.
-- Mario Carneiro
I'm nervous about HOL as a foundation for all of undergraduate mathematics because I want to do linear algebra on tangent spaces of manifolds and I don't see any way of doing this nicely in HOL. It's absolutely clear that HOL is great for some kinds of undergraduate maths and Isabelle/HOL is way ahead of Lean in complex analysis but I believe lean will catch up in the end. As a mathematician I think that classical logic and AC and functional extensionality and propositional extensionality are non-negotiable, that's what is happening in maths departments.
My issue with HOL is that I don't see how to take tensor products of presheaves of modules over a presheaf of rings using the tensor product API. A presheaf of rings on a topological space is a functor from the category of open sets on the space to the category of rings. Because this is a dependent type, it's hard to make this definition and access the ring API for the rings in question in a HOL system (or at least I don't know how to do it). But as far as I know nobody is working on this. Similarly I don't know whether this can be done in a univalent system but here I don't see an obstruction, I just see a community that isn't really interested in the question. Voevodsky used this kind of construction many times in this work but he never got there with his univalent foundations. It's a basic construction in algebraic geometry.
In fact this construction is used all over the proof of FLT, it is used to construct the Picard group of a curve, which is a key construction for the easy direction of the Taniyama Shimura conjecture (making an elliptic curve from a modular form. The hard part, making the form from the curve, was done by Wiles in many cases and it had FLT as a consequence. This uses far deeper facts about the Picard group).
So if you were to try and prove FLT in HOL, you are going to run into a situation where you can't use typeclasses for your rings and modules. At least this is my understanding of it.
-- Kevin Buzzard
But as far as I know nobody is working on this.
I believe the current trick to support this kind of thing in Isabelle/HOL is a mechanism called Types-to-Sets that will translate the entire theory of rings, for example, into theorems about ring-like subsets of a type. These subsets can be as dependent as you like, but they aren't types themselves which is why the actual ring theorems (using a "ring A" typeclass) don't apply.
-- Mario Carneiro
There is a foundational problem with Isabelle/HOL, but the problem is not with lack of type dependencies, it is lack of axiomatic strength. Luckily it is pretty rare to need additional axiomatic strength outside set theory (some might also say category theory but I think category theorists just want naive set theory). Suppose we had type class inference for not just types but also subsets of a type. Then the dependency problem would be solved, and we would be basically working in a soft typed system. This, by the way, is essentially how formalization in ZFC works - ZFC has only one type but it nevertheless has no trouble describing "dependent sets". The problem is that Isabelle/HOL has native support for axiomatic type classes on types, but not on sets. The system will automatically infer that types have these instances, but the set version requires tedious proof. Maybe sledgehammer can handle some of this, but it's not designed for it so some things will time out and it will generally be unpleasant and unpredictable. So working over sets is much more painful than working on types, for no foundational reason. If the system did type class inference for sets too (which is certainly possible) then this wouldn't be a problem.
-- Mario Carneiro
Coq people feel the need to apologize for using classical axioms. Some libraries, like mathcomp, are getting over this, but it's still a distraction. Proof irrelevance is also a very nice to have in lean, as well as quotient types; the Coq workarounds are really not nice.
The lean user interface is nicer than Coq IMO; this is of course important for mathematicians, since they have lower tolerance for unintuitive interfaces than computer scientists.
From my point of view as a logician, Lean is on firmer footing than Coq. The Coq kernel is very large and poorly specified. But most mathematicians don't care about this.
I should mention that all of these issues are being worked on in the Coq community, but Lean had the advantage of being born later and learning from past mistakes.
Finally, there is the circular reason: there are more mathematicians using Lean, so it is more attractive to mathematicians.
and Kevin has done a great job to this end as the designated lean propagandist.
Coq has a constructivist culture. There are many more type theorists among prominent Coq contributors. You could conceivably call me a type theorist but I don't know anyone else in the lean community with major type theory leanings, at least among the big contributors. In the coq community I could point out at least Thierry Coquand, Thorsten Altenkirch, and Dominique Larchey-Wendling as type theorists with strong constructivist leanings.
-- Mario Carneiro
Lean is in an interesting position because it is getting a steady in-flow of classically trained mathematicians.
so it is important that the tool address the problems that the (mathematician) users have.
-- Mario Carneiro