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