El sistema Mizar consiste en un lenguaje formal para escribir definiciones matemáticas y demostraciones, un asistente de demostración , que es capaz de verificar mecánicamente las demostraciones escritas en este lenguaje, y una biblioteca de matemáticas formalizadas , que puede usarse en la demostración de nuevos teoremas. [1] El sistema es mantenido y desarrollado por el Proyecto Mizar, anteriormente bajo la dirección de su fundador Andrzej Trybulec .
En 2009, la Biblioteca Matemática Mizar era el mayor cuerpo coherente de matemáticas estrictamente formalizadas que existía. [2]
El Proyecto Mizar fue iniciado alrededor de 1973 por Andrzej Trybulec como un intento de reconstruir el lenguaje matemático vernáculo para que pueda ser verificado por una computadora. [3] Su objetivo actual, además del desarrollo continuo del Sistema Mizar, es la creación colaborativa de una gran biblioteca de pruebas verificadas formalmente, que cubra la mayor parte del núcleo de las matemáticas modernas. Esto está en línea con el influyente manifiesto QED . [4]
Actualmente, el proyecto es desarrollado y mantenido por grupos de investigación de la Universidad de Białystok (Polonia), la Universidad de Alberta (Canadá) y la Universidad Shinshu (Japón). Si bien el verificador de pruebas Mizar sigue siendo propietario, [5] la Biblioteca Matemática Mizar (el considerable corpus de matemáticas formalizadas que verificó) tiene licencia de código abierto. [6]
Los artículos relacionados con el sistema Mizar aparecen regularmente en las revistas revisadas por pares de la comunidad académica de formalización matemática, entre las que se incluyen Studies in Logic, Grammar and Rhetoric , Intelligent Computer Mathematics , Interactive Theorem Proving , Journal of Automated Reasoning y Journal of Formalized Reasoning .
La característica distintiva del lenguaje Mizar es su legibilidad. Como es común en los textos matemáticos, se basa en la lógica clásica y en un estilo declarativo . [7] Los artículos de Mizar se escriben en ASCII ordinario , pero el lenguaje fue diseñado para ser lo suficientemente cercano al lenguaje matemático vernáculo como para que la mayoría de los matemáticos pudieran leer y entender los artículos de Mizar sin una formación especial. [1] Sin embargo, el lenguaje permite el mayor nivel de formalidad necesario para la verificación automatizada de pruebas .
Para que una prueba sea admitida, todos los pasos deben justificarse ya sea mediante argumentos lógicos elementales o citando pruebas previamente verificadas. [8] Esto da como resultado un nivel de rigor y detalle más alto que el que es habitual en los libros de texto y publicaciones matemáticas. Así, un artículo típico de Mizar es aproximadamente cuatro veces más largo que un artículo equivalente escrito en estilo ordinario. [9]
La formalización es una tarea relativamente laboriosa, pero no imposiblemente difícil. Una vez que uno se familiariza con el sistema, se necesita aproximadamente una semana de trabajo a tiempo completo para lograr que una página de un libro de texto sea verificada formalmente. Esto sugiere que sus beneficios están ahora al alcance de campos aplicados como la teoría de la probabilidad y la economía . [2]
La Biblioteca Matemática Mizar (MML) incluye todos los teoremas a los que los autores pueden hacer referencia en artículos nuevos. Una vez aprobados por el verificador de pruebas, se los evalúa en un proceso de revisión por pares para determinar si su contribución y estilo son apropiados. Si se los acepta, se los publica en la revista asociada Journal of Formalized Mathematics [10] y se los agrega a la MML.
En julio de 2012, la MML incluía 1150 artículos escritos por 241 autores. [11] En total, estos contienen más de 10 000 definiciones formales de objetos matemáticos y alrededor de 52 000 teoremas demostrados sobre estos objetos. Más de 180 hechos matemáticos nombrados han recibido codificación formal de esta manera. [12] Algunos ejemplos son el teorema de Hahn-Banach , el lema de König , el teorema del punto fijo de Brouwer , el teorema de completitud de Gödel y el teorema de la curva de Jordan .
Esta amplitud de cobertura ha llevado a algunos [13] a sugerir a Mizar como una de las principales aproximaciones a la utopía QED de codificar todas las matemáticas fundamentales en una forma verificable por computadora.
Todos los artículos de MML están disponibles en formato PDF como artículos del Journal of Formalized Mathematics . [10] El texto completo de MML se distribuye con el verificador Mizar y se puede descargar gratuitamente desde el sitio web de Mizar. En un proyecto reciente en curso [14], la biblioteca también se puso a disposición en un formato wiki experimental [15] que solo admite ediciones cuando son aprobadas por el verificador Mizar. [16]
El sitio web MML Query [11] implementa un potente motor de búsqueda para el contenido de MML. Entre otras capacidades, puede recuperar todos los teoremas MML demostrados sobre cualquier tipo u operador en particular. [17] [18]
El MML se basa en los axiomas de la teoría de conjuntos de Tarski-Grothendieck . Aunque semánticamente todos los objetos son conjuntos , el lenguaje permite definir y utilizar tipos débiles sintácticos . Por ejemplo, un conjunto puede declararse de tipo Nat solo cuando su estructura interna se ajusta a una lista particular de requisitos. A su vez, esta lista sirve como definición de los números naturales y el conjunto de todos los conjuntos que se ajustan a esta lista se denota como NAT . [19] Esta implementación de tipos busca reflejar la forma en que la mayoría de los matemáticos piensan formalmente en los símbolos [20] y, por lo tanto, agilizar la codificación.
Las distribuciones del Mizar Proof Checker para todos los sistemas operativos principales están disponibles para su descarga gratuita en el sitio web del Proyecto Mizar. El uso del verificador de pruebas es gratuito para todos los fines no comerciales. Está escrito en Free Pascal y el código fuente está disponible en GitHub. [21]