El sistema Mizar consta de un lenguaje formal para escribir definiciones y demostraciones matemáticas, un asistente de pruebas , que puede verificar mecánicamente pruebas 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 la lengua vernácula matemática para que pudiera ser verificada 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 consonancia con el influyente manifiesto QED . [4]
Actualmente, el proyecto lo desarrollan y mantienen 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 importante conjunto de matemáticas formalizadas que verificó) tiene licencia de código abierto. [6]
Artículos relacionados con el sistema Mizar aparecen regularmente en revistas revisadas por pares de la comunidad académica de formalización matemática. Estos incluyen estudios de lógica, gramática y retórica , matemáticas informáticas inteligentes , demostración interactiva de teoremas , Journal of Automated Reasoning y Journal of Formalized Reasoning .
La característica distintiva del idioma Mizar es su legibilidad. Como es común en los textos matemáticos, se basa en la lógica clásica y un estilo declarativo . [7] Los artículos de Mizar están escritos en ASCII ordinario , pero el lenguaje fue diseñado para ser lo suficientemente cercano a la lengua vernácula matemática como para que la mayoría de los matemáticos pudieran leer y comprender 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 estar justificados mediante argumentos lógicos elementales o citando pruebas previamente verificadas. [8] Esto da como resultado un mayor nivel de rigor y detalle de lo 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 normal. [9]
La formalización requiere relativamente mucha mano de obra, pero no es extremadamente difícil. Una vez que uno está versado en el sistema, se necesita aproximadamente una semana de trabajo a tiempo completo para verificar formalmente una 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 . [2]
La Biblioteca Matemática Mizar (MML) incluye todos los teoremas a los que los autores pueden hacer referencia en artículos recién escritos. Una vez aprobados por el verificador de pruebas, se evalúan adicionalmente en un proceso de revisión por pares para determinar su contribución y estilo adecuados. Si se aceptan, se publican en el Journal of Formalized Mathematics [10] asociado y se agregan al MML.
En julio de 2012, el MML incluía 1150 artículos escritos por 241 autores. [11] 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 nombrados se han beneficiado de la codificación formal. [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 básicas 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 del 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 estuvo disponible en un formato wiki experimental [15] que solo admite ediciones cuando son aprobadas por el verificador Mizar. [dieciséis]
El sitio web MML Query [11] implementa un potente motor de búsqueda de contenidos del MML. Entre otras capacidades, puede recuperar todos los teoremas de 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 sintácticos débiles . Por ejemplo, se puede declarar que un conjunto es de tipo Nat sólo 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 conforman 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 sobre los símbolos [20] y así simplificar la codificación.
Las distribuciones de Mizar Proof Checker para todos los principales sistemas operativos están disponibles para su descarga gratuita en el sitio web de Mizar Project. 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]
{{cite book}}: |journal=ignorado ( ayuda ){{cite book}}: |journal=ignorado ( ayuda )