Система Мицар состоит из формального языка для написания математических определений и доказательств, помощника по доказательству , способного механически проверять доказательства, написанные на этом языке, и библиотеки формализованной математики , которую можно использовать при доказательстве новых теорем. [1] Система поддерживается и развивается проектом Mizar Project, ранее находившимся под руководством его основателя Анджея Трибулца .
В 2009 году Математическая библиотека Мицара была крупнейшим из существующих структур строго формализованной математики. [2]
Проект «Мицар» был начат примерно в 1973 году Анджеем Трибулцем как попытка реконструировать математический язык , чтобы его можно было проверить с помощью компьютера. [3] Его текущей целью, помимо постоянного развития системы Мицар, является совместное создание большой библиотеки формально проверенных доказательств, охватывающих большую часть ядра современной математики. Это соответствует влиятельному манифесту QED . [4]
В настоящее время проект разрабатывается и поддерживается исследовательскими группами Белостокского университета (Польша), Университета Альберты (Канада) и Университета Синсю (Япония). Хотя программа проверки доказательств Mizar остается частной собственностью, [5] Математическая библиотека Mizar — значительная часть формализованной математики, которую она проверяла — имеет лицензию с открытым исходным кодом. [6]
Статьи, связанные с системой Мицар, регулярно появляются в рецензируемых журналах академического сообщества по математической формализации. К ним относятся исследования по логике, грамматике и риторике , интеллектуальной компьютерной математике , интерактивному доказательству теорем , журналу автоматизированных рассуждений и журналу формализованного рассуждения .
Отличительной особенностью языка Мицар является его читабельность. Как это обычно бывает в математических текстах, он опирается на классическую логику и декларативный стиль . [7] Статьи Mizar написаны в обычном ASCII , но этот язык был разработан так, чтобы быть достаточно близким к математическому языку, чтобы большинство математиков могли читать и понимать статьи Mizar без специальной подготовки. [1] Тем не менее, язык обеспечивает повышенный уровень формальности, необходимый для автоматической проверки доказательств .
Чтобы доказательство было признано, все шаги должны быть обоснованы либо элементарными логическими аргументами, либо ссылкой на ранее проверенные доказательства. [8] Это приводит к более высокому уровню строгости и детализации, чем это принято в математических учебниках и публикациях. Таким образом, типичная статья Mizar примерно в четыре раза длиннее аналогичной статьи, написанной обычным стилем. [9]
Формализация является относительно трудоемкой, но не такой уж невыполнимой задачей. После того, как человек разбирается в системе, ему потребуется около недели полной занятости для формальной проверки страницы учебника. Это говорит о том, что ее преимущества теперь доступны прикладным областям, таким как теория вероятностей и экономика . [2]
Математическая библиотека Мицара (MML) включает все теоремы, на которые авторы могут ссылаться в новых статьях. После утверждения проверяющим корректуры они дополнительно оцениваются в процессе рецензирования на предмет надлежащего вклада и стиля. В случае принятия они публикуются в соответствующем Журнале формализованной математики [10] и добавляются в MML.
По состоянию на июль 2012 года в MML включено 1150 статей, написанных 241 автором. [11] В совокупности они содержат более 10 000 формальных определений математических объектов и около 52 000 теорем, доказанных на этих объектах. Более 180 названных математических фактов получили пользу от формальной кодификации. [12] Некоторые примеры: теорема Хана-Банаха , лемма Кенига , теорема Брауэра о неподвижной точке , теорема Гёделя о полноте и теорема Жордана о кривой .
Такая широта охвата привела к тому, что некоторые [13] предложили Мицар как одно из ведущих приближений к утопии КЭД, заключающейся в кодировании всей базовой математики в форме, поддающейся компьютерной проверке.
Все статьи MML доступны в формате PDF в виде статей журнала формализованной математики . [10] Полный текст MML распространяется вместе с программой проверки Mizar и его можно бесплатно загрузить с веб-сайта Mizar. В рамках недавнего текущего проекта [14] библиотека также была доступна в экспериментальной вики- форме [15] , которая допускает редактирование только после того, как они одобрены программой проверки Mizar. [16]
Веб-сайт MML Query [11] реализует мощную поисковую систему по содержимому MML. Помимо прочего, он может извлекать все теоремы MML, доказанные для любого конкретного типа или оператора. [17] [18]
MML построен на аксиомах теории множеств Тарского-Гротендика . Несмотря на то, что семантически все объекты являются множествами , язык позволяет определять и использовать синтаксически слабые типы . Например, набор может быть объявлен как набор типа Nat только в том случае, если его внутренняя структура соответствует определенному списку требований. В свою очередь, этот список служит определением натуральных чисел , а совокупность всех множеств, соответствующих этому списку, обозначается как NAT . [19] Такая реализация типов призвана отразить то, как большинство математиков формально думают о символах [20], и тем самым упростить кодификацию.
Дистрибутивы Mizar Proof Checker для всех основных операционных систем доступны для бесплатного скачивания на веб-сайте Mizar Project. Использование средства проверки доказательств бесплатно для всех некоммерческих целей. Он написан на Free Pascal , а исходный код доступен на GitHub. [21]
{{cite book}}
: |journal=
игнорируется ( помощь ){{cite book}}
: |journal=
игнорируется ( помощь )