Systém Mizar je nástroj poskytující formální jazyk pro psaní definic a matematických důkazů, asistent kontroly umožňující automatické ověřování těchto důkazů a knihovna formalizované matematiky.
(en) Oficiální webové stránky