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

Компьютерное доказательство — это математическое доказательство , хотя бы частично созданное компьютером .

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

также предпринимались попытки В области исследований искусственного интеллекта создать более мелкие, явные, новые доказательства математических теорем снизу вверх с использованием методов автоматического рассуждения, таких как эвристический поиск. Такие автоматизированные средства доказательства теорем доказали ряд новых результатов и нашли новые доказательства известных теорем. ^{[ нужна ссылка ]} Кроме того, интерактивные помощники по доказательствам позволяют математикам разрабатывать удобочитаемые доказательства, правильность которых, тем не менее, формально проверяется. Поскольку эти доказательства, как правило, доступны для изучения человеком (хотя и с трудом, как в случае с доказательством гипотезы Роббинса ), они не разделяют противоречивые последствия компьютерных доказательств методом исчерпывания.

Методы

Одним из методов использования компьютеров в математических доказательствах является использование так называемых проверенных чисел или строгих чисел. Это означает численные вычисления, но с математической строгостью. Используется многозначная арифметика и принцип включения. ^{[ объяснить ]} чтобы гарантировать, что многозначный вывод числовой программы включает в себя решение исходной математической задачи. Это делается путем контроля, включения и распространения ошибок округления и усечения, используя, например, интервальную арифметику . Точнее, вычисления сводятся к последовательности элементарных операций, скажем $(+,-,\times ,/)$ . В компьютере результат каждой элементарной операции округляется до компьютерной точности. Однако можно построить интервал, обеспеченный верхней и нижней границей результата элементарной операции. Далее приступают к замене чисел интервалами и выполнению элементарных операций между такими интервалами представимых чисел. ^{[ нужна ссылка ]}

Философские возражения

Доказательства с помощью компьютера являются предметом некоторых споров в математическом мире, и Томас Тимочко первым высказал возражения. Те, кто придерживается аргументов Тимочко, считают, что длинные компьютерные доказательства в некотором смысле не являются «настоящими» математическими доказательствами, поскольку они включают в себя так много логических шагов, что люди практически не поддаются проверке , и что математиков фактически просят замените логический вывод из предполагаемых аксиом доверием к эмпирическому вычислительному процессу, на который потенциально влияют ошибки в компьютерной программе, а также дефекты в среде выполнения и аппаратном обеспечении. ^[1]

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

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

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

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

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

Приложения

Теоремы, доказанные с помощью компьютерных программ

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

Теорема о четырех цветах , 1976 г. ^[2]
Гипотеза Митчелла Фейгенбаума об универсальности в нелинейной динамике. Доказано О.Э. Лэнфордом с использованием строгой компьютерной арифметики, 1982 г.
Connect Four , 1988 — решенная игра
Отсутствие конечной проективной плоскости порядка 10, 1989 г.
Гипотеза о двойном пузыре , 1995 г. ^[3]
Гипотеза Роббинса , 1996 г.
Гипотеза Кеплера , 1998 — проблема оптимальной упаковки сфер в ящик.
Аттрактор Лоренца , 2002 г. - 14-я задача Смейла, доказанная Уорвиком Такером с использованием интервальной арифметики.
17-точечный случай задачи «Счастливый конец» , 2006 г.
Курил ^[4]^[5]^[6] (между 2006 и 2016 годами) вычислил несколько чисел Ван дер Вардена с помощью FPGA на основе SAT-решателя .
NP-твердость триангуляции минимального веса , 2008 г.
Ахмед ^[7]^[8]^[9]^[10]^[11] (между 2009 и 2014 годами) вычислил несколько чисел Ван дер Вардена, используя на основе алгоритма DPLL автономные и распределенные SAT-решатели . Ахмед впервые использовал кластерно-распределенные SAT-решатели , чтобы доказать, что w(2; 3, 17) = 279 и w(2; 3, 18) = 312 в 2010 году. ^[8]
Оптимальные решения кубика Рубика можно получить не более чем за 20 ходов грани, 2010 г. ^[12]
Минимальное количество подсказок для решения судоку — 17, 2012 г.
В 2014 году частный случай проблемы несоответствия Эрдёша был решен с помощью SAT-решателя . Полная гипотеза была позже решена Теренсом Тао без помощи компьютера. ^[13]
Булева задача тройки Пифагора решена с использованием 200 терабайт данных в мае 2016 года. ^[14]
Приложения к теории Колмогорова-Арнольда-Мозера ^[15]^[16]
Свойство Каждана (T) группы автоморфизмов свободной группы ранга не ниже пяти
Шур номер пять , доказательство того, что S(5) = 161, было анонсировано в 2017 году Мариной Хойле и заняло 2 петабайта места. ^[17]^[18]
Гипотеза Келлера в измерении 7 - единственный оставшийся в 2020 году случай с на 200 гигабайт . доказательством ^[19]^[20]
Хроматическое число упаковки бесконечной квадратной сетки равно 15, предложено Subercaseaux и Heule в 2023 году. ^[21]^[22] (См. также: Задача Хадвигера – Нельсона о хроматическом числе плоскости)

См. также

Ссылки

^ Тимочко, Томас (1979), «Проблема четырех цветов и ее математическое значение», The Journal of Philosophy , 76 (2): 57–83, doi : 10.2307/2025976 , JSTOR 2025976 .
^ Гонтье, Жорж (2008), «Формальное доказательство — Теорема о четырех цветах» (PDF) , Уведомления Американского математического общества , 55 (11): 1382–1393, MR 2463991 , заархивировано (PDF) из оригинала в 2011 г. 08-05
^ Хасс, Дж.; Хатчингс, М.; Шлафли, Р. (1995). «Гипотеза о двойном пузыре» . Электронные объявления об исследованиях Американского математического общества . 1 (3): 98–102. CiteSeerX 10.1.1.527.8616 . дои : 10.1090/S1079-6762-95-03001-0 .
^ Курил, Михал (2006). Структура обратного отслеживания для кластеров Беовульфа с расширением для многокластерных вычислений и реализации задач Sat Benchmark (докторская диссертация). Университет Цинциннати.
^ Курил, Михал (2012). «Вычисление числа Ван дер Вардена W (3,4) = 293». Целые числа . 12 : А46. МР 3083419 .
^ Курил, Михал (2015). «Использование кластеров FPGA для вычислений SAT». Параллельные вычисления: на пути к экзафлопсу : 525–532.
^ Ахмед, Танбир (2009). «Несколько новых чисел Ван дер Вардена и несколько чисел типа Ван дер Вардена». Целые числа . 9 : А6. дои : 10.1515/integ.2009.007 . МР 2506138 . S2CID 122129059 .
^ Перейти обратно: ^а ^б Ахмед, Танбир (2010). «Два новых числа Ван дер Вардена w(2;3,17) и w(2;3,18)». Целые числа . 10 (4): 369–377. дои : 10.1515/integ.2010.032 . МР 2684128 . S2CID 124272560 .
^ Ахмед, Танбир (2012). «О вычислении точных чисел Ван дер Вардена». Целые числа . 12 (3): 417–425. дои : 10.1515/integ.2011.112 . МР 2955523 . S2CID 11811448 .
^ Ахмед, Танбир (2013). «Еще несколько чисел Ван дер Вардена». Журнал целочисленных последовательностей . 16 (4): 13.4.4. МР 3056628 .
^ Ахмед, Танбир; Куллманн, Оливер; Сневили, Хантер (2014). «О числах Ван дер Вардена w(2;3,t)» . Дискретная прикладная математика . 174 (2014): 27–51. arXiv : 1102.5433 . дои : 10.1016/j.dam.2014.05.007 . МР 3215454 .
^ «Число Бога — 20» . Cube20.org . Июль 2010 года . Проверено 18 октября 2023 г.
^ Чезаре, Крис (1 октября 2015 г.). «Математик разгадает волшебную загадку» . Природа . 526 (7571): 19–20. Бибкод : 2015Natur.526...19C . дои : 10.1038/nature.2015.18441 . ПМИД 26432222 .
^ Лэмб, Эвелин (26 мая 2016 г.). «Доказательство по математике объемом в двести терабайт — самое большое за всю историю» . Природа . 534 (7605): 17–18. Бибкод : 2016Natur.534...17L . дои : 10.1038/nature.2016.19990 . ПМИД 27251254 .
^ Челлетти, А.; Кьерчия, Л. (1987). «Строгие оценки компьютерной теории КАМ» . Журнал математической физики . 28 (9): 2078–86. Бибкод : 1987JMP....28.2078C . дои : 10.1063/1.527418 .
^ Фигерас, JL; Харо, А.; Луке, А. (2017). «Строгое компьютерное применение теории КАМ: современный подход» . Основы вычислительной математики . 17 (5): 1123–93. arXiv : 1601.00084 . дои : 10.1007/s10208-016-9339-3 . hdl : 2445/192693 . S2CID 28258285 .
^ Хойле, Марин Дж. Х. (2017). «Шур номер пять». arXiv : 1711.08076 [ cs.LO ].
^ «Шур номер пять» . www.cs.utexas.edu . Проверено 6 октября 2021 г.
^ Бракензик, Джошуа; Хойле, Марин; Макки, Джон; Нарваес, Дэвид (2020). «Разрешение гипотезы Келлера». В Пельтье, Николя; Софрони-Стоккерманс, Виорика (ред.). Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 12166. Спрингер. стр. 48–65. дои : 10.1007/978-3-030-51074-9_4 . ISBN 978-3-030-51074-9 . ПМЦ 7324133 .
^ Хартнетт, Кевин (19 августа 2020 г.). «Компьютерный поиск решает 90-летнюю математическую задачу» . Журнал Кванта . Проверено 8 октября 2021 г.
^ Суберказо, Бернардо; Хойле, Марин Дж. Х. (23 января 2023 г.). «Упаковочное хроматическое число бесконечной квадратной сетки равно 15». arXiv : 2301.09757 [ cs.DM ].
^ Хартнетт, Кевин (20 апреля 2023 г.). «Число 15 описывает тайный предел бесконечной сетки» . Журнал Кванта . Проверено 20 апреля 2023 г.

Дальнейшее чтение

Ленат, Д.Б. (1976). АМ: Подход к открытиям в математике с использованием искусственного интеллекта как эвристический поиск (PDF) (доктор философии). Лаборатория искусственного интеллекта, Стэнфордский университет. STAN-CS-76-570, Отчет проекта эвристического программирования HPP-76-8.
Мейер, КР; Шмидт, Д.С., ред. (2012). Компьютерные доказательства в анализе . Тома IMA по математике и ее приложениям. Том. 28. Спрингер. ISBN 978-1-4613-9092-3 .
Накао, М.; Плам, М.; Ватанабэ, Ю. (2019). Численные методы проверки и компьютерные доказательства уравнений в частных производных . Ряд Спрингера по вычислительной математике. Спрингер. ISBN 9789811376696 .

Внешние ссылки

Лэнфорд, Оскар Э. (1982). «Компьютерное доказательство гипотез Фейгенбаума» (PDF) . Бык. амер. Математика. Соц . 6 (3): 427–434. CiteSeerX 10.1.1.434.8389 . дои : 10.1090/S0273-0979-1982-15008-X .
Фурс, Эдмунд (1990). Почему AM выдохлась? (Технический отчет). Кафедра компьютерных исследований Университета Гламоргана. КС-90-4. Архивировано из оригинала 17 июля 2012 г. Проверено 6 сентября 2016 г. {{cite tech report}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )
Бегли, С. (16 апреля 2018 г.). «Цифровые доказательства, выполненные на компьютере, могут ошибаться» . Питтсбург Пост-Газетт . Архивировано из оригинала 16 апреля 2018 г.
«Специальный выпуск о формальных доказательствах» . Уведомления Американского математического общества . Декабрь 2008 года.

[tymoczko-1] Тимочко, Томас (1979), «Проблема четырех цветов и ее математическое значение», The Journal of Philosophy , 76 (2): 57–83, doi : 10.2307/2025976 , JSTOR 2025976 .

[2] Гонтье, Жорж (2008), «Формальное доказательство — Теорема о четырех цветах» (PDF) , Уведомления Американского математического общества , 55 (11): 1382–1393, MR 2463991 , заархивировано (PDF) из оригинала в 2011 г. 08-05

[3] Хасс, Дж.; Хатчингс, М.; Шлафли, Р. (1995). «Гипотеза о двойном пузыре» . Электронные объявления об исследованиях Американского математического общества . 1 (3): 98–102. CiteSeerX 10.1.1.527.8616 . дои : 10.1090/S1079-6762-95-03001-0 .

[kouril2006-4] Курил, Михал (2006). Структура обратного отслеживания для кластеров Беовульфа с расширением для многокластерных вычислений и реализации задач Sat Benchmark (докторская диссертация). Университет Цинциннати.

[kouril2012-5] Курил, Михал (2012). «Вычисление числа Ван дер Вардена W (3,4) = 293». Целые числа . 12 : А46. МР 3083419 .

[kouril2016-6] Курил, Михал (2015). «Использование кластеров FPGA для вычислений SAT». Параллельные вычисления: на пути к экзафлопсу : 525–532.

[ahmed2009-7] Ахмед, Танбир (2009). «Несколько новых чисел Ван дер Вардена и несколько чисел типа Ван дер Вардена». Целые числа . 9 : А6. дои : 10.1515/integ.2009.007 . МР 2506138 . S2CID 122129059 .

[ahmed2010-8] Перейти обратно: ^а ^б Ахмед, Танбир (2010). «Два новых числа Ван дер Вардена w(2;3,17) и w(2;3,18)». Целые числа . 10 (4): 369–377. дои : 10.1515/integ.2010.032 . МР 2684128 . S2CID 124272560 .

[ahmed2011-9] Ахмед, Танбир (2012). «О вычислении точных чисел Ван дер Вардена». Целые числа . 12 (3): 417–425. дои : 10.1515/integ.2011.112 . МР 2955523 . S2CID 11811448 .

[ahmedJIS-10] Ахмед, Танбир (2013). «Еще несколько чисел Ван дер Вардена». Журнал целочисленных последовательностей . 16 (4): 13.4.4. МР 3056628 .

[aks2011-11] Ахмед, Танбир; Куллманн, Оливер; Сневили, Хантер (2014). «О числах Ван дер Вардена w(2;3,t)» . Дискретная прикладная математика . 174 (2014): 27–51. arXiv : 1102.5433 . дои : 10.1016/j.dam.2014.05.007 . МР 3215454 .

[12] «Число Бога — 20» . Cube20.org . Июль 2010 года . Проверено 18 октября 2023 г.

[13] Чезаре, Крис (1 октября 2015 г.). «Математик разгадает волшебную загадку» . Природа . 526 (7571): 19–20. Бибкод : 2015Natur.526...19C . дои : 10.1038/nature.2015.18441 . ПМИД 26432222 .

[14] Лэмб, Эвелин (26 мая 2016 г.). «Доказательство по математике объемом в двести терабайт — самое большое за всю историю» . Природа . 534 (7605): 17–18. Бибкод : 2016Natur.534...17L . дои : 10.1038/nature.2016.19990 . ПМИД 27251254 .

[15] Челлетти, А.; Кьерчия, Л. (1987). «Строгие оценки компьютерной теории КАМ» . Журнал математической физики . 28 (9): 2078–86. Бибкод : 1987JMP....28.2078C . дои : 10.1063/1.527418 .

[16] Фигерас, JL; Харо, А.; Луке, А. (2017). «Строгое компьютерное применение теории КАМ: современный подход» . Основы вычислительной математики . 17 (5): 1123–93. arXiv : 1601.00084 . дои : 10.1007/s10208-016-9339-3 . hdl : 2445/192693 . S2CID 28258285 .

[17] Хойле, Марин Дж. Х. (2017). «Шур номер пять». arXiv : 1711.08076 [ cs.LO ].

[18] «Шур номер пять» . www.cs.utexas.edu . Проверено 6 октября 2021 г.

[19] Бракензик, Джошуа; Хойле, Марин; Макки, Джон; Нарваес, Дэвид (2020). «Разрешение гипотезы Келлера». В Пельтье, Николя; Софрони-Стоккерманс, Виорика (ред.). Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 12166. Спрингер. стр. 48–65. дои : 10.1007/978-3-030-51074-9_4 . ISBN 978-3-030-51074-9 . ПМЦ 7324133 .

[20] Хартнетт, Кевин (19 августа 2020 г.). «Компьютерный поиск решает 90-летнюю математическую задачу» . Журнал Кванта . Проверено 8 октября 2021 г.

[21] Суберказо, Бернардо; Хойле, Марин Дж. Х. (23 января 2023 г.). «Упаковочное хроматическое число бесконечной квадратной сетки равно 15». arXiv : 2301.09757 [ cs.DM ].

[22] Хартнетт, Кевин (20 апреля 2023 г.). «Число 15 описывает тайный предел бесконечной сетки» . Журнал Кванта . Проверено 20 апреля 2023 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]