[NB see also “Lean has real manifolds!” ;-), written 5 months later]
There are loads of computer theorem provers. There is Lean, there is Coq, there is Agda, Idris, Isabelle-HOL, HOL-Light, UniMath, Mizar and many others. Which one is the best one for formalising a proof of Fermat’s Last Theorem?
I’ve spent the last few months having a good look at all of these systems and I think that out of all the ones which are currently on offer to us (the mathematical community) the one which offers most hope is Lean. I checked Lean’s suitability by defining perfectoid spaces in Lean 3 with Patrick Massot and Johan Commelin, two other mathematicians — and it worked fine. We ran into a lot of problems along the way, but in essentially every situation the problem we were in was of our own making, and we were rescued by computer scientists who know nothing of perfectoid spaces but who are on the other hand very well equipped to answer extremely specific technical questions and give us extremely specialised advice about how best to turn mathematics into functional programming in practice.
But we still don’t have smooth real manifolds. I was initially perplexed by why things were going so slowly; I saw a definition from first principles as an undergraduate. But now I understand the reason, and it’s a bit bizarre. The reason is that a general principle in Lean is that one should set things up in as much generality as possible, for certain efficiency reasons which are of no interest to mathematicians. A more precise explanation is of course the extremely specialised advice offered to us by the computer scientists in this situation. This has an unfortunate consequence that you can’t just wait for an Imperial undergraduate to do it 😦 One apparently really needs to think about differentiating maps between some quite general real topological vector spaces, at least some of which can be infinite-dimensional. This kind of stinks, but that’s the way it is with dependent type theory. Important: I am not saying that real manifolds can’t or won’t be done in Lean. I am just saying that we know what to do but it is taking a long time and it is more technical than one might guess at first. We’ll get there. Thank you to (in alphabetical order) Jeremy Avigad, Sebastien Gouezel, Patrick Massot, Zhouhang Zhou and all the others who are making steady progress. We have recently reached a milestone — we have defined the Bochner Integral. I don’t know what that is. Although when thinking about it in Lean I ended up so confused that I had to confess on mathoverflow that I didn’t even really understand the real numbers.
Xena 
How ‘quite general’ are your topological vector spaces? I have a coauthor who works on manifolds modelled on arbitrary locally convex spaces, and they don’t seem to have many problems. If you want references, I can supply.
LikeLike
All I know is that they just got the Bochner integral. I am no analyst.
LikeLike
Could you go into more detail about your investigation of the other systems, and what you prefer about Lean?
LikeLike
I find this weirdly reassuring, since I feel like I too do not really understand the definition of smooth manifold as well as I understand anything algebraic.
LikeLike
I do think it’s interesting that we have all this Bourbaki stuff on topological rings and a whole lot of applications e.g. adic spaces, perfectoid spaces, with presheaves and sheaves etc, in Lean, but we still don’t have a theory of differentiation which everyone is happy with yet. However again let me stress that serious progress is being made.
LikeLike
On what basis do you conclude that “the one which offers most hope is Lean”. In my experience almost all of these types of systems require more than a few months experience to get a feel for what they can do.
LikeLike
That is a fair question. All systems have problems. First let’s talk about the background logic. History seems to indicate that type theory is a more popular choice than set theory, so I ruled out the set theory based provers. Lack of dependent types seems to make things like sheaves of abelian groups on a topological space very hard to do, so I ruled out the simple type theory systems. Out of the dependent type theory systems, Lean has the advantage over Coq and the others in that it has all the things that mathematicians want and computer scientists might not supply: quotients, functional extensionality, the axiom of choice, the law of the excluded middle and so on. Lean also seems to have the most “modern abstract maths” (schemes, group cohomology, perfectoid spaces etc) which is in my mind concrete evidence that it is suitable for modern mathematics. Finally there is UniMath and the other HoTT systems. HoTT has an elegant solution to a problem which classical dependent type theory runs into, namely rewriting along isomorphisms. However Lean will one day offer a different kind of solution to this, and we will have to wait and see how well this works. However what concerns with UniMath is that whilst it has been around for a while and has a ton of category theory, it hasn’t seemed to have made much impact in other areas of mathematics.
I am a mathematician. I want to see things like the Hodge conjecture, or even real manifolds, in my theorem provers. I am not seeing these things in *any theorem prover at all* right now, however there are people actively working on this sort of thing in Lean, and I don’t see this kind of activity happening with other theorem provers.
I know that this sort of topic is great for flame wars, but there’s my take on it, and if you have another take I would be more than happy for you to explain it here. I’m not trying to say “I’m right” but I am saying “I chose Lean”.
LikeLiked by 1 person