В 2014 году два математика из Ливерпульского университета, Великобритания, Алексей Лисица и Борис Конев, обратили внимание на интересную проблему – если компьютер приводит доказательство математической задачи, которое слишком велико для изучения, то как судить, насколько оно верное?
В своей статье (eng), учёные описывают написание и запуск компьютерной программы для решения малой части задачи, известной как задача несоответствия Эрдеша.
Математики, решая подобные задачи, исписывают целые тома своими нетривиальными доказательствами. Любой, прошедший курс высшей математики, может это подтвердить. Вполне понятно их стремление переложить на надёжные плечи машин генерацию наиболее приземлённых частей своего творчества.
Конечно, математиков терзали смутные сомнения, что когда-нибудь, в один из не самых прекрасных дней, компьютер будет работать не очень долго, а результат его работы будет очень велик. И вот этот день настал. Результат работы программы Лисицы и Конева поражает воображение – файл с текстом доказательства занял объём в 13 гигабайт - объём объем сравнимый с объемомо информации в Википедии.
Перед научным миром возникла диллема: либо принимать на веру доказательства, созданные машинами, как факт (хотя мы не в состоянии их проверить), либо отказаться от их использования, ограничивая тем самым наши возможности. Как поступить?
На самом деле, эта проблема далеко не новая. Еще в 19 веке была сформулирована теорема о четырёх красках, которая утверждает, что всякую расположенную на плоскости или на сфере карту можно раскрасить не более чем четырьмя разными цветами (красками) так, чтобы любые две области с общим участком границы были раскрашены в разные цвета. При этом области должны быть односвязными, а под общим участком границы понимается часть линии, то есть стыки нескольких областей в одной точке не считаются общей границей для них.
Доказана она была лишь в 1976 году Кеннетом Аппелем (англ.) и Вольфгангом Хакеном (англ.) из Иллинойского университета. И это была первая крупная математическая теорема, доказанная с помощью компьютера. При этом, доказательство было принято не всеми математиками, поскольку его невозможно проверить вручную. В дальнейшем оно получило более широкое признание, хотя у некоторых долгое время оставались сомнения.
Комментарии ()