Доказательство математических теорем

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

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

Гипотеза четырех красок была впервые выдвинута Фрэнсисом Гутри в 1852 г. и, невзирая на применение множества оригинальных и изобретательных мат. идей, не поддавалась доказательству до тех пор, пока, наконец, спустя столетие Аппель и Хакен не пустили в ход способности И. и. Гипотеза четырех красок кратко формулируется следующим образом: «Для раскрашивания любой карты т. о., чтобы соседние страны с общей границей имели разные цвета, достаточно четырех красок».

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

«В этот момент программа, теперь уже насыщенная нашими идеями и усовершенствованиями за 2 прошедших года, начала удивлять нас. Поначалу мы старались проверять ее аргументы вручную, с тем чтобы можно было предсказать курс, к-рому она последует в тон или иной ситуации, но теперь она вдруг начала действовать подобно шахматной ЭВМ. Она прорабатывала сложные стратегии, опирающиеся на все те приемы, к-рым она «научилась», и зачастую эти подходы были гораздо более искусными и умелыми, чем те, что предприняли бы мы сами. Тем самым она начала учить нас вещам в отношении возможных продолжений, к-рые оказывались для нас совершенно неожиданными. В каком-то смысле она превзошла своих создателей в определенных аспектах «интеллектуальных», а тж технических сторон этой задачи.»

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

Революционное применение И. и. вызвало острые споры как среди математиков, так и среди философов. Аппель и Хакен выразили свое отношение к проблемам доказательства математиком и доказательства компьютером в следующих словах:

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

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

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

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

Изменяется ли «смысл основополагающего понятия доказательства» или изменяется только субъект доказательства, — это стратегический вопрос для математиков и философов, однако интеллектуальные последствия искусственного мат. интеллекта вполне могут оказать радикальное влияние на внедрение подобных исслед. во всех дисциплинах.