Deus ex machina: как компьютеры ищут Бога

Теорема о четырех красках

В 1852 году Фрэнсис Гатри, молодой английский математик, увлекся, казалось бы, детской забавой. Вооружившись карандашами, он разукрашивает карту графств Британии так, чтобы на ней не оказалось граничащих областей одного цвета. После многих попыток математик понимает, что для этого всегда хватает четырех красок, и даже обобщает свой вывод, утверждая, что данное правило применимо ко всем возможным картам.

Гатри пытается найти доказательство, но безуспешно. Вскоре он рассылает письмо со своей догадкой знакомым математикам и отплывает в Южную Африку. Там он становится адвокатом, увлекается ботаникой, а потом снова возвращается к математике. Фрэнсис Гатри умирает в 1899 году, навсегда увековечив свое имя лишь в названии описанного им вида вереска Erica guthriei. Теорема о четырех красках будет доказана только спустя сто с лишним лет.

Нельзя сказать, что все эти годы математики бездействовали: появлялось много ошибочных и неполных доказательств или успешных работ для разных частных случаев. Так, в 1890 году лектор Дурхэмского университета Перси Джон Хивуд доказал, что для подходящего оформления любой карты всегда хватит пяти красок. А уже в XX веке было доказано, что достаточно и четырех, но только для карт с 25, 26, 35 или даже 39 областями.

Компьютерные доказательства в математике

Полное непротиворечивое доказательство появилось только в 90-х годах прошлого века. Американские математики Аппель и Хаккен на нескольких сотнях страниц свели всю задачу к перебору тысячи конфигураций: если получится разукрасить эти карты четырьмя красками, то это автоматически означает верность теоремы для всех возможных карт.

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

Компьютерные доказательства уже не редкость в современной математике. Ведь что такое доказательство? Из ограниченного и непротиворечивого набора утверждений нужно, руководствуясь установленными правилами логики, получить утверждение конечное. Пройти путь, например, от аксиом Евклидовой геометрии («От всякой точки до всякой точки можно провести прямую» и т. д.) до теоремы Пифагора («В прямоугольном треугольнике квадрат длины гипотенузы равен сумме квадратов длин катетов»).

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

Ансельм Кентерберийский и компьютер

Ансельм Кентерберийский, средневековый философ и богослов XI–XII веков, за свою жизнь сформулировал множество доказательств существования Бога. Два утверждения, от которых отталкивается одно из них, упрощенно можно сформулировать так:

1. Бог — это самое совершенное из всех явлений.

2. Идея Бога заложена в нашем сознании.

Но, говорит Ансельм Кентерберийский, идея и одновременное физическое существование гораздо более совершенно, чем просто идея. А значит, Бог как самое совершенное существо реален, а не только обитает в нашем разуме.

Позднее многие критиковали это доказательство, что для обычного человека совсем не удивительно: существование Творца здесь, получается, выводится из самой идеи о Нем. Впрочем, компьютер, как показала работа Поля Оппенгеймера и Эдварда Залта из Стэнфорда, в этой логической цепочке противоречий и изъянов не увидел.

Для проверки положений Ансельма Кентерберийского исследователи использовали систему автоматического доказательства теорем Prover9. В качестве своеобразных аксиом они загрузили в систему два исходных утверждения средневекового философа. После вычислений компьютер выдал свой вердикт: все корректно.

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

Вычисляющая Вселенная

«Для человека с молотком все похоже на гвоздь, для человека с компьютером — на вычисление», — заявил в своем выступлении на TEDx немецкий ученый Юрген Шмидхубер и показал маленький листочек с записанными на нем законами физики, по которым вычисляется наша Вселенная.

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

В 1967 году немецкий инженер Конрад Цузе впервые сформулировал гипотезу, согласно которой наша Вселенная есть лишь гигантское вычисление, запущенное кем-то неизвестным со времен Большого взрыва. Идея пришлась по вкусу многим ученым. Так, Сет Ллойд, американский физик из Массачусетского технологического института, недавно даже выпустил книгу «Вычисляющая Вселенная». В ней весь наш мир представляется гигантским квантовым компьютером, ведущим свои вычисления по фундаментальным законам физики — своеобразным аналогам правил логики, по которым тот же Prover9 пытается доказать математическую теорему.

Вселенные без нас

Один взмах крыла бабочки миллионы лет назад способен поменять очень многое: динозавры доживут до наших дней, Барак Обама не станет президентом США, в Москве выпадет майский снег. Рэй Брэдбери в своем рассказе «И грянул гром» придумал одну из самых запоминающихся метафор современной науки.

Так, даже небольшие изменения в начальных условиях для вычисления Вселенной, которые аналогичны тем самым исходным утверждениям для компьютерных доказательств теорем, могут привести нас в совершенно другие миры. Что определяет эти условия, пока непонятно. Случайности. Крохотные флуктуации в распределении энергии по Вселенной сразу после Большого взрыва: будь они хоть чуть-чуть другими — мы сразу получим какой-нибудь необитаемый мир с антигравитацией.

Эти фокусы, по мысли Шмидхубера, должны поменять наш взгляд на случайности. Возьмем, к примеру, число пи — отношение длины любой окружности к длине ее диаметра. Десятичная дробь, выражающая эту константу, больше всего похожа на бесконечное нагромождение цифр. Но есть не одна и не две формулы, с помощью которых можно вычислить каждую из этих, казалось бы, случайных цифр. (Правда, чем больше мы захотим узнать, тем больше времени нам потребуется.)

Выходит, можно написать программу, которая по несложной формуле, из рациональных предпосылок будет однозначно определять весь хаос числа пи. А значит, и программа Вселенной (начальные условия плюс фундаментальные законы физики) может однозначно вычислить весь наш мир от первой его секунды и до настоящего момента.

Рождение Солнца, появление земной атмосферы, ваш вчерашний завтрак — все это неминуемо было заложено в программе Вселенной. И никого из нас оттуда не выкинуть, как не выкинуть ни одну из бесконечных цифр числа π. Без нас Вселенная невозможна. Во всяком случае, так считают некоторые компьютерные теологи.