2 ms·
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
by smokel 3mo 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.
[1] https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system
- robinzfc 3mo agoMizar 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). [1] https://reference-global.com/issue/FORMA/33/1 https://reference-global.com/issue/FORMA/33/1