The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

You have (conveniently) chosen not to address my examples in current mathematical literature, where there’d be issues with AC.

Perelman did not accept the Fields Medal (but he was offered it).

These are things I’m aware of but choose not to mention, except maybe for cultural fascination.

Whilst I have no doubt that LEM and AC will be thoroughly embedded in the Perelman proof, I believe that this has nothing to do with the fact that the proof of the Poincaré conjecture "seems particularly tricky to formalise"

I wasn't talking about AC in this section of my note.

[...] 

This will clearly never happen and we need another approach.

I agree with this, broadly. If it's too painful to formalize using current technology, the solution isn't to brute-force it by throwing lots of money at it, but it is, rather, to make it easier to formalize.

The fact that LEM and AC are still some sort of an "issue" in formalisation -- still something worth talking about -- makes the subject feel to the Fields Medal crowd like it is living 100 years in the past; [...]

Oh, it’s not living in the past. We’re talking about a new field of mathematical inquiry: a new foundation for mathematics, far more advanced than plain ZFC. I’d urge you to have a look at Jacob Lurie’s Higher Topos Theory, and Michael Shulman’s 2019 inquiry into HoTT and Quillen model categories that cites HTT several times. The math is stunningly beautiful. Lurie’s field of inquiry is an upcoming field called spectral algebraic geometry. His 2019 work on Ultracategories supplies a modern proof to a Stone-type duality theorem, the Makkai duality theorem.

Yes, it is a niche field because it is a new field, but it is very much active. And much of the research eventually ends up in Coq’s HoTT, which replaces everything down to Coq’s stdlib. HoTT started with Vladimir Voevodsky, who was incidentally also a Fields Medalist.

Lean is essentially a Computer Algebra system with a pCIC frontend: the computation done in the VM is essentially a “hack”, since it hasn't been formalized before implementation. It has the potential to become a mainstream “programming language for doing math” with an active development community; Lean4 is written mostly in Lean, with a C++ stage0. And yes, it is very good at doing a lot of advanced-undergraduate level mathematics today.

Obviously, building new foundations for mechanized mathematics can take a while.

R.