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.

▲

kevinbuzzard 10 days ago | parent [-]

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".

▲

daxfohl 9 days ago | parent [-]

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.

	▲	kevinbuzzard 9 days ago \| parent [-]
		Right now I would say that tools like Lean are not useful for learning advanced mathematics, currently you're mostly better off with pencil and paper. This might change but right now the infrastructure/tools aren't there to make experimenting with new and advanced concepts any easier than it would be on pen and paper.