Sistemul Mizar este un instrument care oferă un limbaj formal pentru scrierea definițiilor și a dovezilor matematice, un asistent de verificare care permite verificarea automată a acestor dovezi și o bibliotecă de matematică formalizată.
(ro) Site oficial