The first computer proof assistant, called Automath, used type theory to encode mathematics on a computer.
Перший комп'ютерний асистент, називався Automath, використовував теорію типів для кодування математики на комп'ютері.