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]
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/
Mizar is actually available under a GPL 3 license (thus FLOSS) from 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