logoalt Hacker News

Western007/31/20251 replyview on HN

Better https://en.wikipedia.org/wiki/Mizar_system Many books create, many proof


Replies

fjfaase07/31/2025

I understand that the Mizar community is rather closed and primarily focused on extending the Mizar Mathematical Library. The Mizar proof checker is closed source.

Lean is gaining traction, which can be seen from the fact that at the moment 81 [1] of the 100 theorems of the 'Formalizing 100 Theorems' [1] have been proven in Lean, while Mizar stands at 71 [3]

[1] https://leanprover-community.github.io/100.html

[2] https://www.cs.ru.nl/%7Efreek/100/

[3] https://mizar.uwb.edu.pl/100/

show 1 reply