[smokel]

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

[robinzfc]

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

[1] https://reference-global.com/issue/FORMA/33/1