3 ms·
Better https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system Many books create, many proof
by Western0 1y ago
Better https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system
Many books create, many proof
- fjfaase 1y agoI 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 https://leanprover-community.github.io/100.html [2] https://www.cs.ru.nl/%7Efreek/100/ https://www.cs.ru.nl/%7Efreek/100/ [3] https://mizar.uwb.edu.pl/100/ https://mizar.uwb.edu.pl/100/
- zozbot234 1y agoMizar is actually available under a GPL 3 license (thus FLOSS) from https://github.com/MizarProject/system https://github.com/MizarProject/system . There's an experimental Rust reimplementation that's at least 5x faster than the original: https://github.com/digama0/mizar-rs https://github.com/digama0/mizar-rs