[Nzen]

For a perspective of a mathematician that came to evangelize theorem provers, I recommend Kevin Buzzard's MS 2019-09 presentation [0] about LEAN. He highlights cultural misunderstanding and apathy on both sides of the domain divide. He also references the idea that the people who might make the appropriate tools may not have stayed in academia. So, he's structured his courses around using LEAN with the indirect consequence that power users (undergrads) may choose to become open source committers.

[0] https://www.youtube.com/watch?v=Dp-mQ3HxgDE One hour of presentation and then 15 min of q/a. My favorite is around 1:04:00 when someone asks a second time why he disprefers coq, and Buzzard complains that it can't represent some advanced quotient type that he'd have to work around. I'm reminded of [1]

[1] https://prog21.dadgum.com/160.html Dangling by a trivial feature

[abstractcontrol]

Having been inspired by that video by Kevin Buzzard and finally finding something that would be worth formalizing, I am trying out Lean at the moment. I have about 2-3 months of Coq experience, so I can say that even without the quotient type, Lean is much better designed than Coq. I can't vouch for how it will do at scale since I've only started it out, but from what I can see, Lean fixes all the pain points that I had with Coq while going through Software Foundations.

It has things like structural recursion (similar to Agda), dependent pattern matching (the biggest benefit of which would be proper variable naming), unicode, `calc` blocks, good IDE experience (it actually has autocomplete) with VS Code (I prefer it over Emacs and the inbuilt CoqIDE is broken on Windows), mutually recursive definitions and types, and various other things that are not at the top of my head.

If I were to sum it up, the biggest issue with Coq is that it does not allow you to structure your code properly. This is kind of a big thing for me as a programmer.

[morningseagulls]

>My favorite is around 1:04:00 when someone asks a second time why he disprefers coq, and Buzzard complains that it can't represent some advanced quotient type that he'd have to work around. I'm reminded of [1]

>[1] https://prog21.dadgum.com/160.html Dangling by a trivial feature

Second what abstractcontrol said.[0] I wouldn't say being able to deal with quotient types is a "trivial" feature, because Buzzard does explain his reason for why quotient types are crucial for what he does.

The motivation is that he wants to formalise a concept that is the subject of current active research, instead of yet another concept from undergraduate mathematics. In this case, it's the notion of perfectoid spaces,[1] which was only introduced in 2012 by Peter Scholze.[2]

The justification for this is sociological: research mathematicians predominantly find the retreading of old ground boring and trivial. Buzzard wants to sell the power of theorem provers to exactly these mathematicians, so he felt that formalising something that many number theorists would be intensely interested in may have more impact.

Unfortunately, while I'd like to think that he's succeeded somewhat, the reaction I've seen is just more of the "well, isn't that nice" variety, outside of some enthusiasts, many of whom are young and/or not very influential. Mainly, it's because theorem provers still can't help mathematicians improve their productivity, because there's still a lot of stuff that's still missing in the ecosystem, and Buzzard pointed out some of the missing "features" that may help theorem provers take off.

[0] https://news.ycombinator.com/item?id=21239067

[1] https://en.wikipedia.org/wiki/Perfectoid_space

[2] https://en.wikipedia.org/wiki/Peter_Scholze

[hollerith]

I watch that video on your recommendation and am glad I did.