| ▲ | smokel 4 hours ago | |
Lean is the Mizar here. For those who have no clue what this is about, Mizar [1] was an early automated theorem prover. Can't wait for HN to add AI features to explain concepts in the sideline, and autovoting. | ||
| ▲ | robinzfc 3 hours ago | parent [-] | |
Mizar is an early theorem prover. It still exists, see the 2025 issue of Formalized Mathematics journal [1] that publishes math articles formally verified by Mizar (since 1990). | ||