Metamath fue iniciado por Norman Megill en 1993. El sitio web de Metamath incluye teoremas matemáticos de varios campos dentro de las matemáticas. Cada teorema se establece y se prueba en el lenguaje Metamath.
Una cita de la página de inicio de Metamath , página de inicio de Metamath :
Mini FAQQ: ¿Qué es Metamath?
R: Metamath es un lenguaje pequeño que puede expresar teoremas en matemáticas abstractas, acompañado de pruebas que pueden ser verificadas por un programa de computadora. Este sitio tiene una colección de páginas web generadas a partir de esas pruebas y le permite ver las matemáticas desarrolladas con todo detalle a partir de los primeros principios, con rigor absoluto. Esperemos que te divierta, te sorprenda y posiblemente te ilumine de una manera especial.
A continuación, un ejemplo de prueba. Para ver lo que expresan estas matemáticas abstractas en este pequeño lenguaje, veamos un ejemplo. Este lo seleccioné al azar. Es la prueba de la desigualdad del triángulo para números complejos, abstrii – Metamath Proof Explorer.
- ¿Cómo visualizan los físicos y los matemáticos el espacio-tiempo y cómo la gravedad lo deforma?
- ¿Quién es matemático?
- ¿Cuáles son algunos de los problemas no resueltos en Matemáticas, que cuando se resuelvan, tendrán un profundo efecto en el mundo de la Física?
- ¿Cuáles son los teoremas hermosos menos conocidos?
- En gráfico, ¿qué es la pendiente? ¿Cuál es el uso de ello?
La prueba es de 48 líneas de largo. Cada declaración tiene una justificación con un enlace. La afirmación a probar es
[matemáticas] | A + B | \ leq | A | + | B | [/ matemáticas]
donde [matemáticas] A [/ matemáticas] y [matemáticas] B [/ matemáticas] son números complejos. Aquí está el comienzo de la prueba. 
Las líneas 1 y 2 postulan que A y B son números complejos. La línea 3 dice que el conjugado complejo de B es un número complejo (porque la conjugación compleja es una operación en números complejos). La línea 4 dice que A multiplicado por el conjugado complejo de B es un número complejo (ya que la multiplicación es una operación en números complejos). La línea 5 dice que la parte real de ese último número es menor o igual que su valor absoluto (citando un teorema anterior).
Algunas de estas son declaraciones bastante largas, como la línea 25, pero la longitud se debe en parte a que todas las expresiones están entre paréntesis. La prueba es muy larga porque cada término en una expresión necesita una justificación para escribirlo.
Tenga en cuenta que hay diferentes niveles en la prueba. Varían del 1 al 9 en esta prueba. No es obvio lo que significan. Son los niveles de los árboles. Metamath usa solo una regla lógica, la sustitución. La prueba podría mostrarse como un árbol en lugar de una lista, y los niveles le indican qué tan alto en el árbol va la línea en particular. El nivel alcanza 1 cuando la prueba se completa en la línea 47.
¿Para qué sirve Metamat?
Es un sistema interesante. El verificador de pruebas de Metamath ha verificado que las pruebas son correctas. No es un comprobador de teoremas automatizado. La gente construye los teoremas.
No parece la mejor manera de aprender matemáticas, ya que los humanos usan varias reglas lógicas de inferencia, y la sustitución es solo una de ellas. Es interesante que una regla sea suficiente, pero tener una sola regla complica las explicaciones, y la explicación es uno de los principales propósitos de las pruebas.
Debido a que este sistema usa solo una regla de inferencia, un programa para verificar las pruebas puede ser corto. Desde la página web de Metamath:
Raph Levien escribió independientemente el verificador de prueba mmverify notablemente pequeño en Python. Él escribe: “Encuentro todo un poco mágico. Esas 300 líneas de código, más un par de docenas de axiomas, te dan los bloques de construcción para todas las matemáticas”.
Metamath es impresionante, pero prefiero ver un sistema más rico de reglas de inferencia, incluso si eso requiere más programación para verificar las pruebas.
Si tuviera algo de tiempo extra, creo que sería divertido repasar algunas de las pruebas en Metamath, y tal vez presentar algunas de las mías para algo que no está cubierto.