Automath: мова, у якій машина перевіряє математику
У листопаді 1968 року Н. Г. де Брейн випустив у Технічному університеті Ейндговена звіт про Automath — мову для запису математики так докладно, що комп'ютер може перевірити, чи правильний текст. Такий текст може містити не лише доведення однієї теореми, а цілу теорію разом із її правилами виведення.
Чому це важливо
Замість того щоб шукати доведення, машина стала перевіряти доведення, написане людиною, рядок за рядком. Це інша половина машинного доведення, і саме на ній стоять пізніші системи перевірки, зокрема числення конструкцій, яке його автори прямо виводять з формалізмів Automath.
За звітом, Automath — не мова програмування: кожен текст, написаний за її правилами, стверджує правильну математику. Процесори для перевірки написано на ALGOL; автор дякує Л. С. ван Бентем Ютінгу й Л. Г. Ф. К. ван Бре. Звіт каже, що комп'ютер ніколи не повинен приймати неправильний рядок, і що процесор, який працював у листопаді 1968 року, обходився без підказок, але досвід був ще дуже обмежений. Чисел звіт не наводить. Перша велика перевірка відбулася пізніше, і її описує дисертація ван Бентем Ютінга, захищена 1 березня 1977 року: переклад «Основ аналізу» Ландау, близько 500 сторінок, перевірено на Burroughs B6700 в Ейндговені, останню сторінку — у вересні 1975 року, усю книжку — остаточним прогоном 18 жовтня 1975 року. Прогін тривав 2 години, з них 42 хвилини — перевірка; 13 433 рядки, 215 138 виразів, 2 519,7 секунди перевірки. Чого запис не стверджує: скільки теорем Ландау перевірено — дисертація такого числа не називає.