Comment by harperlee
3 days ago
Perhaps this thread is a good place to ask, could anyone contribute their own opinion about the relative future of lean vs. idris/coq/agda? I want to dedicate some time to this from a knowledge representation point of view, but I'm unsure about which of them will have less risk of ending up as so many esoteric languages... I sank a lot of time on clojure core.logic for a related project and got burnt with the low interest / small community issue already, so I've been hesitant to start with any of them for some time.
IME Lean and Coq/Rocq are used more in practice, and have bigger libraries and communities, than Idris and Agda.
Rocq is the most common for program verification, but I suspect mainly due to it being older, and it has weird quirks due to its age, so Lean may catch up. Lean is the most common for proving mathematical theorems.
Big projects verified in Rocq include CompCert, CertiCoq, and sel4. Additionally, some large companies use Rocq to verify critical software like in airplanes (there's a list at https://github.com/ligurio/practical-fm although it may not be accurate). Big projects in Lean include mathlib (collection of various mathematical proofs), and the ongoing work to prove Fermat's Last Theorem (https://imperialcollegelondon.github.io/FLT/) and PFR (https://teorth.github.io/pfr/). I'm not aware of "real-world" projects in Idris and Agda but may be wrong.
That said, they're all small communities compared to something like C++ or JavaScript. Moreover, verifying programs is very slow and tedious (relative to writing them), so I wouldn't be surprised if we see a big breakthrough (perhaps with AI) that fundamentally changes the landscape. But remember that even with a breakthrough your skills may be transferable.
I wouldn't put much money on any of them. IME most mathematicians aren't that interested in formalization, and the gulf between a hand written proof and and a computer verified syntax is pretty huge.
Theyre interesting to learn and play with for their own sake, but I'd be reluctant to make any bets on the future of any of them.
If I had to choose, Lean seems to have the most momentum, though the others have been around longer and each has some loyal users.
Most mathematicians aren't doing formalization themselves, but my impression is that a lot of them are watching with interest. I get asked "is my job secure?" quite a lot nowadays. Answer is "currently yes".
Okay, yeah my response is ultimately based on the one conversation about it that I've had with the one prof of the one math class I've taken in the last 30 years, so take that with a grain of salt.
(Tangentially, I'm so so so so angry that universities stopped offering remote classes after covid. I'd been wanting to take a bunch of classes for a long time, but it's just not feasible when you've got a full-time job in the 'burbs. I managed to get through measure theory and quantum mechanics while the window was open, and it was great. I planned to get through a few more in differential geometry and algebraic topology, but then the window closed. Feels like I'll pretty much have to wait until retirement at this point. Oh well, first-world problems.)
Edit: oh and actually, follow-up question: are these tools useful for _learning_ advanced mathematics? I looked up in Lean and its approach to topology is very non-standard, which makes me question whether I'd actually be learning math or whether I'd mainly be learning how to finagle things into Lean-friendly representations but missing the higher-level concepts.
1 reply →