Система Mizar: Формализация математических знаний и доказательств.
Mizar system
Mizar: формальный язык для математических доказательств, ассистент проверки и библиотека формализованной математики. Проект Mizar – крупнейшая база верифицированных теорем.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Система Mizar состоит из формального языка для записи математических определений и доказательств, средства проверки доказательств, способного механически проверять доказательства, написанные на этом языке, и библиотеки формализованной математики, которая может использоваться при доказательстве новых теорем. Система поддерживается и разрабатывается проектом Mizar, ранее под руководством её основателя Анджея Трибулеца. В 2009 году Математическая библиотека Mizar была крупнейшим единым корпусом строго формализованной математики, существовавшим на тот момент.
the star system
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec. In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.
История
Проект Mizar был начат около 1973 года Анджеем Трибулеком как попытка реконструировать математический язык, чтобы его можно было проверить с помощью компьютера. Его текущая цель, помимо непрерывного развития системы Mizar, — совместное создание обширной библиотеки формально верифицированных доказательств, охватывающей большую часть основ современной математики. Это соответствует влиятельному манифесту QED. В настоящее время проект разрабатывается и поддерживается исследовательскими группами Белостокского университета (Польша), Университета Альберты (Канада) и Университета Шиншу (Япония). Хотя проверяющий доказательства Mizar остаётся проприетарным, Математическая библиотека Mizar — значительный корпус формализованной математики, верифицированный системой — распространяется под лицензией открытого исходного кода. Статьи, посвящённые системе Mizar, регулярно публикуются в рецензируемых журналах научного сообщества, занимающегося математической формализацией. К ним относятся Studies in Logic, Grammar and Rhetoric, Intelligent Computer Mathematics, Interactive Theorem Proving, Journal of Automated Reasoning и Journal of Formalized Reasoning.
The Mizar Project was started around 1973 by Andrzej Trybulec as an attempt to reconstruct mathematical vernacular so it can be checked by a computer. Its current goal, apart from the continual development of the Mizar System, is the collaborative creation of a large library of formally verified proofs, covering most of the core of modern mathematics. This is in line with the influential QED manifesto. Currently the project is developed and maintained by research groups at Białystok University, Poland, the University of Alberta, Canada, and Shinshu University, Japan. While the Mizar proof checker remains proprietary, the Mizar Mathematical Library—the sizable body of formalized mathematics that it verified—is licensed open source. Papers related to the Mizar system regularly appear in the peer reviewed journals of the mathematic formalization academic community. These include Studies in Logic, Grammar and Rhetoric, Intelligent Computer Mathematics, Interactive Theorem Proving, Journal of Automated Reasoning and the Journal of Formalized Reasoning.
Мизарский язык
Отличительной чертой языка Mizar является его читаемость. Как и в математических текстах, он основывается на классической логике и декларативном стиле. Статьи на Mizar написаны в обычном ASCII, но язык был разработан таким образом, чтобы быть достаточно близким к математической терминологии, чтобы большинство математиков могли читать и понимать статьи на Mizar без специальной подготовки. Это обеспечивает более высокий уровень строгости и детализации, чем обычно встречается в математических учебниках и публикациях. Таким образом, типичная статья на Mizar примерно в четыре раза длиннее эквивалентной работы, написанной в обычном стиле. Формализация требует значительных усилий, но не является непосильной задачей. После освоения системы, для формальной верификации одной страницы учебника требуется около недели полной занятости. Это позволяет предположить, что его преимущества становятся доступными для таких прикладных областей, как теория вероятностей и экономика, и добавлены в MML.
The distinctive feature of the Mizar language is its readability. As is common in mathematical text, it relies on classical logic and a declarative style. Mizar articles are written in ordinary ASCII, but the language was designed to be close enough to the mathematical vernacular that most mathematicians could read and understand Mizar articles without special training. This results in a higher level of rigor and detail than is customary in mathematical textbooks and publications. Thus, a typical Mizar article is about four times as long as an equivalent paper written in ordinary style. Formalization is relatively labor intensive, but not impossibly difficult. Once one is versed in the system, it takes about one week of full time work to have a textbook page formally verified. This suggests that its benefits are now in the reach of applied fields such as probability theory and economics. and added to the MML.
Ширина
По состоянию на июль 2012 года MML включал 1150 статей, написанных 241 автором. В совокупности они содержат более 10 000 формальных определений математических объектов и около 52 000 теорем, доказанных для этих объектов. Более 180 именованных математических фактов выиграли от формального кодирования. Примеры включают теорему Хана — Банаха, лемму Кёнига, теорему Брауэра о неподвижной точке, теорему Гёделя о полноте и теорему Жордана о кривой. Такая широта охвата заставила некоторых рассматривать Mizar как одно из ведущих приближений к утопии QED — кодированию всей фундаментальной математики в форме, проверяемой компьютером.
As of July 2012, the MML included 1150 articles written by 241 authors. In aggregate, these contain more than 10,000 formal definitions of mathematical objects and about 52,000 theorems proved on these objects. More than 180 named mathematical facts have so benefited from formal codification. Some examples are the Hahn–Banach theorem, Kőnig's lemma, Brouwer fixed point theorem, Gödel's completeness theorem and Jordan curve theorem. This breadth of coverage has led some to suggest Mizar as one of the leading approximations to the QED utopia of encoding all core mathematics in computer verifiable form.
Логическая структура
MML базируется на аксиомах теории множеств Тарского-Гротендика. Хотя семантически все объекты являются множествами, язык позволяет определять и использовать синтаксические слабые типы. Например, множество может быть объявлено типа Nat только если его внутренняя структура соответствует определенному набору требований. В свою очередь, этот набор требований служит определением натуральных чисел, а множество всех множеств, удовлетворяющих этим требованиям, обозначается как NAT. Эта реализация типов призвана отразить то, как большинство математиков формально рассуждают о символах, и тем самым упростить формализацию.
The MML is built on the axioms of the Tarski–Grothendieck set theory. Even though semantically all objects are sets, the language allows one to define and use syntactical weak types. For example, a set may be declared to be of type Nat only when its internal structure conforms with a particular list of requirements. In turn, this list serves as the definition of the natural numbers and the set of all the sets that conform to this list is denoted as NAT. This implementation of types seeks to reflect the way most mathematicians formally think of symbols and so streamline codification.
Проверка доказательств Mizar
Распространения системы проверки доказательств Mizar для всех основных операционных систем свободно доступны для скачивания на веб-сайте проекта Mizar. Использование системы проверки доказательств бесплатно для всех некоммерческих целей. Она написана на Free Pascal, а исходный код доступен на GitHub.
Distributions of the Mizar Proof Checker for all major operating systems are freely available for download at the Mizar Project website. Use of the proof checker is free for all non commercial purposes. It is written in Free Pascal and the source code is available on GitHub.