Comment by raphlinus
14 hours ago
People interested in alternatives to Lean should also look at Metamath. It has nowhere near the adoption that Lean is getting, but is holding its own in [100] theorems results.
It has some advantages and compelling properties, not least of which is that it's very simple, so much so that there are many implementations of checkers; most other proof systems are ultimately defined by a single implementation. It's also astonishingly efficient — the entire database can be checked in less than a second. Set theory is also a familiar foundation for mathematicians, though the question of which is a better foundation compared with type theory is very controversial. Mario Carneiro pushed forward the development of Metamath in his thesis [0].
There are downsides also, including junk theorems, and automation is weaker. It's possible that types really help with the latter. Even so, I think it's worthy of study and understanding.
No comments yet
Contribute on Hacker News ↗