Automath Notes

by Alex Nelson,

Nicolaas Govert de Bruijn invented Automath in 1967, and worked on it over the next 20 years. (Work ended when de Bruijn retired, since he was the fire powering the Automath engine.) It amounts to a glorified typed-lambda calculus, and can rightly be considered the “assembly language” of mathematics.

Currently, the only working interpreter for Automath may be found on Freek Wiedijk’s site. It’s quite fast compared to modern theorem provers, but provides zero automation. (Another reason why “assembly language” is an apt metaphor.)