Sistema mizar

El sistema Mizar consta de un lenguaje formal para escribir definiciones y demostraciones matemáticas, un asistente de demostraciones, que es capaz de comprobar mecánicamente demostraciones escritas en este lenguaje, y una biblioteca de matemáticas formalizadas, que puede utilizarse en la demostración de nuevos teoremas. El sistema es mantenido y desarrollado por Mizar Project, anteriormente bajo la dirección de su fundador Andrzej Trybulec.

En 2009, la Biblioteca Matemática de Mizar era el mayor cuerpo coherente de matemáticas estrictamente formalizadas que existe.

Historia

El Proyecto Mizar fue iniciado alrededor de 1973 por Andrzej Trybulec como un intento de reconstruir la lengua vernácula matemática para que pueda ser verificada por una computadora. 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 cubre la mayor parte del núcleo de las matemáticas modernas. Esto está en línea con el influyente manifiesto QED.

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 de Shinshu, Japón. Si bien el verificador de pruebas de Mizar sigue siendo propietario, la biblioteca matemática de Mizar, el cuerpo considerable de matemáticas formalizadas que verificó, tiene licencia de código abierto.

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. Estos incluyen Estudios en lógica, gramática y retórica, Matemáticas informáticas inteligentes, Demostración interactiva de teoremas, Revista de razonamiento automatizado y el Diario de Razonamiento Formalizado.

Idioma Mizar

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. Los artículos de Mizar están escritos en ASCII ordinario, pero el lenguaje fue diseñado para estar lo suficientemente cerca de la lengua vernácula matemática para que la mayoría de los matemáticos puedan leer y comprender los artículos de Mizar sin una formación especial. Sin embargo, el lenguaje permite el mayor nivel de formalidad necesario para la verificación de pruebas automatizada.

Para que una prueba sea admitida, todos los pasos deben estar justificados ya sea por argumentos lógicos elementales o citando pruebas previamente verificadas. Esto da como resultado un mayor nivel de rigor y detalle que el habitual en los libros de texto y publicaciones de matemáticas. Por lo tanto, un artículo típico de Mizar es aproximadamente cuatro veces más largo que un artículo equivalente escrito en estilo ordinario.

La formalización es relativamente laboriosa, pero no imposiblemente difícil. Una vez que uno está versado en el sistema, se necesita aproximadamente una semana de trabajo a tiempo completo para verificar formalmente la página de un libro de texto. Esto sugiere que sus beneficios están ahora al alcance de campos aplicados como la teoría de la probabilidad y la economía.

Biblioteca Matemática Mizar

La biblioteca matemática de Mizar (MML) incluye todos los teoremas a los que los autores pueden hacer referencia en artículos escritos recientemente. Una vez aprobados por el corrector de pruebas, se evalúan más en un proceso de revisión por pares para determinar la contribución y el estilo apropiados. Si se aceptan, se publican en el Journal of Formalized Mathematics asociado y se agregan a la MML.

Amplitud

En julio de 2012, la MML incluía 1150 artículos escritos por 241 autores. En conjunto, 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 con nombre se han beneficiado de la codificación formal. 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 a sugerir Mizar como una de las principales aproximaciones a la utopía de QED de codificar todas las matemáticas básicas en forma verificable por computadora.

Disponibilidad

Todos los artículos de MML están disponibles en formato PDF como artículos del Journal of Formalized Mathematics. El texto completo de la MML se distribuye con el verificador de Mizar y se puede descargar gratuitamente desde el sitio web de Mizar. En un proyecto reciente en curso, la biblioteca también estuvo disponible en forma de wiki experimental que solo admite ediciones cuando son aprobadas por el verificador de Mizar.

El sitio web MML Query implementa un potente motor de búsqueda de los contenidos de la MML. Entre otras habilidades, puede recuperar todos los teoremas de MML probados sobre cualquier tipo u operador en particular.

Estructura lógica

La 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 sintácticos débiles. Por ejemplo, se puede declarar que un conjunto es del tipo Nat solo cuando su estructura interna cumple con 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 conforman esta lista se denota como NAT. Esta implementación de tipos busca reflejar la forma en que la mayoría de los matemáticos piensan formalmente sobre los símbolos y, por lo tanto, simplifican la codificación.

Comprobador de pruebas Mizar

Las distribuciones de Mizar Proof Checker para todos los principales sistemas operativos están disponibles gratuitamente para su descarga en el sitio web del Proyecto Mizar. El uso del comprobador de pruebas es gratuito para todos los fines no comerciales. Está escrito en Free Pascal y el código fuente está disponible para todos los miembros de la Asociación de Usuarios de Mizar.