Automath ("matemáticas automatizadas") 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 exactitud.
El sistema Automath incluía muchas nociones novedosas que luego fueron adoptadas y/o reinventadas en áreas como el cálculo lambda tipificado y la sustitución explícita . Los tipos dependientes son un ejemplo destacado. Automath fue también 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 tipo ); de Bruijn desconocía el trabajo de Howard y declaró la correspondencia de forma independiente. [1]
LS van Benthem Jutting, como parte de este Ph.D. tesis en 1976, tradujo los Fundamentos del análisis de Edmund Landau al Automath y comprobó su exactitud.
Sin embargo, Automath nunca recibió mucha publicidad en ese momento, por lo que nunca logró un uso generalizado; no obstante, resultó 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 está en uso activo, fue influenciado por Automath.