Comment by 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