Automath ("automatización de las matemáticas") es un lenguaje formal , ideado por Nicolaas Govert de Bruijn a partir de 1967, para expresar teorías matemáticas completas de tal manera que un verificador de pruebas automatizado incluido pueda verificar su corrección.
El sistema Automath incluía muchas nociones novedosas que luego fueron adoptadas y/o reinventadas en áreas como el cálculo lambda tipado y la sustitución explícita . Los tipos dependientes son un ejemplo destacado. Automath también fue el primer sistema práctico que explotó la correspondencia Curry-Howard . Las proposiciones se representaban como conjuntos (llamados "categorías") de sus pruebas, y la cuestión de la demostrabilidad se convirtió en una cuestión de no vacuidad ( habitación de tipos ); de Bruijn desconocía el trabajo de Howard y planteó la correspondencia de forma independiente. [1]
LS van Benthem Jutting, como parte de su tesis doctoral en 1976, tradujo los Fundamentos del análisis de Edmund Landau al autómata y verificó su corrección.
Sin embargo, Automath nunca fue ampliamente publicitado en su momento, por lo que nunca logró un uso generalizado; no obstante, demostró ser muy influyente en el desarrollo posterior de marcos lógicos y asistentes de prueba . [2] [3] El sistema Mizar , un sistema de escritura y verificación de matemáticas formalizadas que todavía se encuentra en uso activo, fue influenciado por Automath.