Система Mizar — набор инструментов, который состоит из формального декларативного языка для записи математических определений и доказательств, помощника по доказательству (который способен автоматически проверять доказательства) и библиотек формализованной математики. Система поддерживается и развивается проектом Mizar, ранее находившимся под руководством его основателя Анджея Трибулеца.
В 2009 году Математическая библиотека Mizar признана крупнейшим из существующих единым собранием строго формализованной математики.
Примечания
Категория:Инструменты интерактивного доказательства теорем