Система Mizar
-
Система Mizar
- Mizar — это формальный язык для математических определений и доказательств с автоматическим помощником проверки.
- Проект Mizar поддерживается и развивается, его цель — создание большой библиотеки формализованных доказательств.
-
История и развитие
- Проект Mizar был начат в 1973 году с целью создания математического языка, поддающегося компьютерной проверке.
- В 2009 году библиотека Mizar была крупнейшей в мире по строго формализованной математике.
- Проект разрабатывается исследовательскими группами из разных стран, а математическая библиотека MML является открытым исходным кодом.
-
Язык Mizar
- Язык Mizar отличается читабельностью и опирается на классическую логику.
- Статьи в Mizar написаны в ASCII, но близки к математическому жаргону.
- Доказательства в Mizar должны быть обоснованы логически или ссылками на проверенные доказательства.
-
Математическая библиотека MML
- MML включает все теоремы, которые могут быть использованы в статьях.
- На июль 2012 года библиотека содержала более 10 000 определений и 52 000 теорем.
- MML охватывает более 180 математических фактов, включая теорему Хана-Банаха.
-
Доступность и структура
- Статьи MML доступны в формате PDF и могут быть загружены с веб-сайта.
- Библиотека также доступна в экспериментальной вики-форме с возможностью редактирования после одобрения.
- MML Query предоставляет мощную поисковую систему для содержимого библиотеки.
-
Логическая структура и проверка
- MML основан на аксиомах теории множеств Тарского-Гротендика.
- Язык позволяет определять слабые типы, отражающие формальное отношение математиков к символам.
- Программа Mizar Proof Checker доступна для бесплатного использования и доступна для скачивания на GitHub.
-
Ссылки и рекомендации
- В статье упоминаются другие системы, такие как Изабель и Метамат.
- Ссылки на официальный веб-сайт проекта Mizar предоставлены в конце статьи.
Полный текст статьи: