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

Математическое доказательство, по крайней мере частично созданное компьютером

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

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

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

Методы

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

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

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

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

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

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

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

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

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

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

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

Смотрите также

• Формальная проверка
• Логик-теоретик
• Математическое доказательство
• Метамат
• Проверка модели
• Семнадцать или перебор
• Символическое вычисление
• Проверенные числовые данные

Ссылки

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

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

• Lenat, DB (1976). AM: Подход искусственного интеллекта к открытию в математике как эвристический поиск (PDF) (PhD). AI Lab., Стэнфордский университет. STAN-CS-76-570, Отчет о проекте эвристического программирования HPP-76-8.
• Мейер, К. Р.; Шмидт, Д. С., ред. (2012). Компьютерные доказательства в анализе. Тома ИМА по математике и ее приложениям. Том 28. Springer. ISBN 978-1-4613-9092-3.
• Накао, М.; Плам, М.; Ватанабэ, Й. (2019). Численные методы проверки и компьютерные доказательства для уравнений с частными производными. Springer Series in Computational Mathematics. Springer. ISBN 9789811376696.

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

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