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

Математики уже обжигались на таких ошибках. В 1992 году оксфордские физики воспользовались эвристическими методами и, исходя из теории струн, высказали некоторые предположения относительно числа алгебраических конструкций, которые могут быть определены в многомерных геометрических пространствах. Математики отнеслись к этому предсказанию с подозрением – откуда физикам знать о столь абстрактных объектах? – и считали, что их сомнения оправдались, когда появилось доказательство, опровергающее эту гипотезу. Оказалось, однако, что в доказательстве содержалась компьютерная составляющая, основанная на программе, в которой была ошибка. Правы были физики, а не математики. Их ввела в заблуждение ошибка в программе. Несколько лет спустя математики сумели доказать (на этот раз без помощи компьютера), что физики были правы.

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

Если речь идет о доказательстве по-настоящему важном, проверка обычно выявляет все нестыковки или ошибки. Именно поэтому премию за решение «задач тысячелетия» присуждают через два года после публикации: считается, что двадцати четырех месяцев должно быть достаточно для выявления любой ошибки. Взять хотя бы первое доказательство Великой теоремы Ферма Эндрю Уайлса. Рецензенты нашли в нем ошибку еще до того, как оно было напечатано. Чудо заключается в том, что Уайлс сумел исправить эту ошибку с помощью своего бывшего ученика Ричарда Тейлора. Но сколько может существовать других ошибочных доказательств, из-за которых мы возводим свои математические здания на ложном фундаменте?

Некоторые новые доказательства настолько сложны, что математики опасаются, что в них могут остаться труднообнаружимые ошибки. Вот, к примеру, классификация конечных простых групп – теорема, близкая к теме моих собственных исследований. Это своего рода периодическая система симметричных атомов, из которых могут быть построены все симметричные объекты. Ее называют «теоремой-монстром», потому что доказательство занимает 10 000 страниц и 100 журнальных статей, в работе над которыми участвовали сотни математиков. В список атомов входят 26 странных и необычных форм, которые называются спорадическими простыми группами. Всегда существовало смутное подозрение, что может существовать и 27-я такая группа, которая, возможно, была пропущена в доказательстве. Способен ли компьютер помочь нам проверить такое сложное доказательство?

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

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

В целом на основании той же индукции! Мы можем привести множество примеров, в которых принцип индукции порождал, по-видимому, справедливые научные теории. Это позволяет нам заключить (методом индукции), что индукция – действенный подход к занятиям наукой.

Coq – проверщик доказательств

По мере появления все новых и новых доказательств, полученных при помощи компьютерных программ, стала ощущаться необходимость в каких-то средствах, позволяющих убедиться, что этим программам можно доверять. В прошлом математические выкладки, созданные людьми, могли проверить люди. Теперь же нужно было создать новые программы для проверки программ, создающих доказательства, так как люди уже не могли проверять их вычисления – они были слишком сложны.