Metamath es un lenguaje diminuto que puede expresar teoremas en matemáticas abstractas, acompañado de pruebas que pueden ser verificadas por un programa de computadora.
Conoce esta herramienta.
Funcionalidad
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 absoluto rigor.Enseñanza - Aprendizaje
Metamath es un lenguaje formal y un programa informático asociado (un verificador de pruebas)para archivar, verificar y estudiar pruebas matemáticas.Tutoriales
vikidia
Ventajas:
- La base de datos más grande de teoremas probados sigue la teoría de conjuntos ZFC convencional y la lógica clásica.
- El sitio web de Metamath también alberga algunas bases de datos más antiguas que ya no se mantienen.
Desventajas:
- El lenguaje Metamath no tiene una lógica específica incrustada en él.
- Toda la página está en ingles .
Licencia:
- Software gratuito.