Система Mizar состоит из формального языка для записи математических определений и доказательств, помощника по доказательству , который способен механически проверять доказательства, написанные на этом языке, и библиотеки формализованной математики , которая может использоваться при доказательстве новых теорем. [1] Система поддерживается и развивается проектом Mizar, ранее под руководством его основателя Анджея Трибулеца .
В 2009 году Математическая библиотека Мицара была крупнейшим из существующих целостных сборников строго формализованной математики. [2]
Проект Mizar был начат около 1973 года Анджеем Трибулецем как попытка реконструировать математический язык , чтобы его можно было проверить с помощью компьютера. [3] Его текущая цель, помимо постоянного развития системы Mizar, заключается в совместном создании большой библиотеки формально проверенных доказательств, охватывающих большую часть ядра современной математики. Это соответствует влиятельному манифесту QED . [4]
В настоящее время проект разрабатывается и поддерживается исследовательскими группами в Белостокском университете (Польша), Альбертском университете (Канада) и Университете Синсю (Япония). В то время как средство проверки доказательств Mizar остается фирменным [5], математическая библиотека Mizar — значительный объем формализованной математики, которую он проверял — лицензирована как open-source. [6]
Статьи, связанные с системой Мицар, регулярно появляются в рецензируемых журналах академического сообщества математической формализации. К ним относятся Studies in Logic, Grammar and Rhetoric , Intelligent Computer Mathematics , Interactive Theorem Proving , Journal of Automated Reasoning и Journal of Formalized Reasoning .
Отличительной чертой языка Mizar является его читабельность. Как это часто бывает в математических текстах, он опирается на классическую логику и декларативный стиль . [7] Статьи Mizar написаны в обычном ASCII , но язык был разработан так, чтобы быть достаточно близким к математическому языку, чтобы большинство математиков могли читать и понимать статьи Mizar без специальной подготовки. [1] Тем не менее, язык обеспечивает повышенный уровень формальности, необходимый для автоматизированной проверки доказательств .
Для того, чтобы доказательство было принято, все шаги должны быть обоснованы либо элементарными логическими аргументами, либо цитированием ранее проверенных доказательств. [8] Это приводит к более высокому уровню строгости и детализации, чем принято в математических учебниках и публикациях. Таким образом, типичная статья в Mizar примерно в четыре раза длиннее эквивалентной статьи, написанной в обычном стиле. [9]
Формализация относительно трудоемка, но не невыполнимо сложна. Как только человек освоится в системе, ему потребуется около недели полной занятости, чтобы формально проверить страницу учебника. Это говорит о том, что ее преимущества теперь доступны прикладным областям, таким как теория вероятностей и экономика . [2]
Математическая библиотека Mizar (MML) включает все теоремы, на которые авторы могут ссылаться в новых написанных статьях. После одобрения проверяющим они далее оцениваются в процессе рецензирования на предмет соответствующего вклада и стиля. Если они приняты, они публикуются в соответствующем журнале Journal of Formalized Mathematics [10] и добавляются в MML.
По состоянию на июль 2012 года MML включал 1150 статей, написанных 241 автором. [11] В совокупности они содержат более 10 000 формальных определений математических объектов и около 52 000 теорем, доказанных об этих объектах. Более 180 названных математических фактов получили формальную кодификацию таким образом. [12] Вот некоторые примеры: теорема Хана–Банаха , лемма Кёнига , теорема Брауэра о неподвижной точке , теорема Гёделя о полноте и теорема о жордановой кривой .
Такая широта охвата привела некоторых [13] к предположению, что Мицар является одним из ведущих приближений к утопии КЭД , заключающейся в кодировании всей базовой математики в форме, поддающейся компьютерной проверке.
Все статьи MML доступны в формате PDF в качестве статей журнала Journal of Formalized Mathematics . [10] Полный текст MML распространяется с помощью программы проверки Mizar и может быть свободно загружен с веб-сайта Mizar. В текущем недавнем проекте [14] библиотека также была сделана доступной в экспериментальной форме вики [15], которая допускает только правки, одобренные программой проверки Mizar. [16]
Сайт MML Query [11] реализует мощную поисковую систему для содержимого MML. Среди других возможностей, он может извлекать все теоремы MML, доказанные для любого конкретного типа или оператора. [17] [18]
MML построен на аксиомах теории множеств Тарского–Гротендика . Хотя семантически все объекты являются множествами , язык позволяет определять и использовать синтаксические слабые типы . Например, множество может быть объявлено как имеющее тип Nat только тогда, когда его внутренняя структура соответствует определенному списку требований. В свою очередь, этот список служит определением натуральных чисел , а множество всех множеств, соответствующих этому списку, обозначается как NAT . [19] Эта реализация типов стремится отразить способ, которым большинство математиков формально думают о символах [20] , и таким образом упростить кодификацию.
Дистрибутивы Mizar Proof Checker для всех основных операционных систем доступны для бесплатной загрузки на веб-сайте проекта Mizar. Использование proof checker бесплатно для всех некоммерческих целей. Он написан на Free Pascal , а исходный код доступен на GitHub. [21]