Le système Automath apportait de nombreuses notions novatrices qui ont été adoptées ou réinventées ultérieurement, comme la substitution explicite ou la notion de type dépendant dont Automath est un exemple paradigmatique. Automath était aussi le premier système pratique qui exploitait ...