Код креативности. Как искусственный интеллект учится писать, рисовать и думать

Доказательство этой теоремы было довольно устрашающим. В нем было 255 страниц, и его публикация заняла целый выпуск журнала Pacific Journal of Math. До его появления доказательства по большей части занимали не более нескольких страниц, и в них можно было разобраться за день. Это же доказательство было таким длинным и сложным, что понять его было непростой задачей для любого математика. Учитывая его размеры, нельзя было не заподозрить, что где-то среди его многочисленных страниц может таиться какая-нибудь малозаметная ошибка.

Поэтому проверка этого доказательства при помощи Coq не только продемонстрировала бы мастерство этой системы: она укрепила бы нашу уверенность в справедливости доказательства одной из самых сложных теорем в математике. Это была достойная цель. Но преобразование доказательства, созданного человеком, в проверяемый код делало эту задачу еще более грандиозной. Гонтье предстояла нелегкая работа.

Он смущенно вспоминал:

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

После совещания один из программистов просмотрел доказательство. О своих впечатлениях он написал Гонтье по электронной почте: «Число строк – 170 000. Число определений – 15 000. Число теорем – 4300. Развлечений – масса!» Группа из кембриджского отделения Microsoft Research потратила на работу над этим доказательством шесть лет. Гонтье рассказывал о том восторге, который он ощущал по мере приближения проекта к завершению. Наконец, после множества бессонных ночей, он мог успокоиться.

«Математика – одна из последних великих романтических дисциплин, – сказал он, – в которой одному гению, по сути дела, приходится держать в голове и понимать сразу всё». Но аппаратное обеспечение человека подходит к пределу своих возможностей. Гонтье надеется, что его работа положит начало эпохе большего доверия и устойчивого сотрудничества между человеком и машиной.

Ограничения «аппаратных средств» человека

Среди молодых математиков сейчас растет ощущение, что многие области математического мира становятся настолько дремучими и сложными, что все три года аспирантуры можно потратить только на то, чтобы понять ту задачу, которую поставил тебе научный руководитель. Можно работать долгие годы, осваивая эту территорию и отмечая на карте свои открытия, а затем обнаружить, что ни у кого другого нет ни сил, ни времени пройти тем же путем, чтобы понять или проверить их.

Повторение чужой работы – дело не слишком благодарное. Однако именно на нем основывается рецензирование статей в научных журналах. Карьерный рост и получение постоянной научной работы зависят от признания, которое дает публикация работ в журналах уровня Annals of Mathematics[71] или Les Publications mathématiques de l’IHES[72]

. Поэтому роль систем, подобных Coq, в проверке доказательств теорем, претендующих на публикацию в таких журналах, может становиться все более значительной.

Некоторым из математиков кажется, что мы подходим к концу эпохи. Та математика, в которой способен ориентироваться человеческий разум, неизбежно должна иметь пределы. Взять хотя бы классификацию конечных простых групп, составных элементов симметрии. Тот факт, что мы, люди, сумели при помощи собственного разума, карандаша и бумаги построить симметричный объект, который может быть построен только в 196 833-мерном пространстве, поразителен. Те математики, которые по-настоящему уверенно разбираются в симметриях группы-монстра, стареют. Подобно средневековым каменщикам, они владеют мастерством, которое будет утрачено с их смертью. У тех, кто идет за ними, нет особого стимула повторять эти готические шедевры, если только они не открывают дорогу к новым чудесам.

Сотни страниц журнальных статей, написанные в течение трех столетий, чтобы доказать, что уравнения Ферма не имеют решений, свидетельствуют о том, какую долгую игру способен вести человеческий разум. И все же при работе над доказательством гипотезы всегда возникает смутное ощущение, что сложность доказательства может превосходить пределы физических возможностей человеческого мозга. Мы способны на поразительные свершения, но математика бесконечна, а мы конечны: мы можем математически доказать, что математика больше, чем можем быть мы.