Я отчасти мог понять, почему это достижение так радует Виньялса. Его проект похож на обучение алгоритма джазовой импровизации, только выбирается не оптимальная следующая нота, а оптимальный следующий логический шаг. Алгоритм существенно расширил возможности компьютера. Он освоил новую территорию. Компьютер создал новые теоремы – как если бы он сочинил новую музыку.

Однако, должен признать, я уходил из DeepMind несколько разочарованным. Казалось бы, такое ускорение прогресса математики должно было привести меня в полный восторг, но я увидел лишь бездумную машинную штамповку математической жвачки, а не услышал волнующую меня музыку сфер. Никто не пытался оценить значение вновь открытых утверждений, никого не интересовало, содержатся ли в них какие-либо откровения. Они были новыми, и только. Казалось, что в них недостает двух третей того, что составляет акт творчества.

Математический тест Тьюринга

Неужели будущее предстанет именно таким? Вернувшись к себе, я попытался прочитать доказательства некоторых из моих любимых теорем в библиотеке «Мицар». Они оставили меня равнодушным. Более того, они привели меня в замешательство, потому что я ничего в них не ощутил. Я с трудом разбирал тот невразумительный формальный язык, на котором они написаны. Наверное, я испытывал приблизительно то же, что по большей части ощущают люди, открывающие одну из моих статей и видящие в ней череду символов, кажущихся бессмысленными. Эти доказательства записаны в виде машинного кода, который позволяет алгоритму совершать формальные переходы от одного истинного утверждения к другому. Компьютеру именно это и требуется, но люди говорят о математике по-другому. Например, вот взятое из «Мицара» доказательство существования бесконечного количества простых чисел:

reserve n, p for Nat;

theorem Euclid: ex p st p is prime & p > n proof

set k = n! + 1;

n! > 0 by NEWTON:23;

then n! >= 0 + 1 by NAT1:38; then k >= 1 + 1 by

REAL1:55;

then consider p such that

A1: p is prime & p divides k by INT2:48; A2: p 0 & p > 1

by A1, INT2: def 5; take p;

thus p is prime by A1;

assume p