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

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

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

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

Методы

Один из методов использования компьютеров в математических доказательствах - это так называемые проверенные числа или точные цифры. Это означает численные вычисления, но с математической строгостью. Один использует многозначную арифметику и принцип включения[прояснить ] чтобы гарантировать, что многозначный вывод числовой программы включает решение исходной математической задачи. Это достигается путем управления, включения и распространения ошибок округления и усечения с использованием, например, интервальная арифметика. Точнее, вычисление сводится к последовательности элементарных операций, например . В компьютере результат каждой элементарной операции округляется точностью компьютера. Однако можно построить интервал, определяемый верхней и нижней границами результата элементарной операции. Затем переходят к замене чисел интервалами и выполнению элементарных операций между такими интервалами представимых чисел.[нужна цитата ]

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

Основная статья: Доказательство, не подлежащее обследованию

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

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

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

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

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

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

Приложения

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

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

Теоремы на продажу

В 2010 году ученые Эдинбургский университет предлагал людям возможность «купить свою собственную теорему», созданную с помощью компьютерного доказательства. Эта новая теорема будет названа в честь покупателя.[7][8]

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

использованная литература

  1. ^ Тимочко, Томас (1979), «Задача четырех цветов и ее математическое значение», Журнал Философии, 76 (2): 57–83, Дои:10.2307/2025976, JSTOR  2025976.
  2. ^ Хасс Дж., Хатчингс М. и Шлафли Р. (1995). Гипотеза о двойном пузыре. Объявления об электронных исследованиях Американского математического общества, 1 (3), 98-102.
  3. ^ Чезаре, Крис (1 октября 2015 г.). «Математик разгадывает загадку мастера». Природа. 526 (7571): 19–20. Bibcode:2015Натура 526 ... 19С. Дои:10.1038 / nature.2015.18441. PMID  26432222.
  4. ^ Лэмб, Эвелин (26 мая 2016 г.). «Математическое доказательство в двести терабайт - самое большое доказательство». Природа. 534 (7605): 17–18. Bibcode:2016Натура.534 ... 17л. Дои:10.1038 / природа.2016.19990. PMID  27251254.
  5. ^ Целлетти А. и Чиеркия Л. (1987). Строгие оценки компьютерной теории КАМ. Журнал математической физики, 28 (9), 2078-2086.
  6. ^ Фигерас, Дж. Л., Аро, А., и Луке, А. (2017). Строгое компьютерное применение теории КАМ: современный подход. Основы вычислительной математики, 17 (5), 1123-1193.
  7. ^ «Статья в Herald Gazette о покупке собственной теоремы». Herald Gazette Scotland. Ноябрь 2010. Архивировано с оригинал 21 ноября 2010 г.
  8. ^ "Сайт школы информатики Эдинбургского университета". Школа информатики Эдинбургского университета. Апрель 2015 г.[постоянная мертвая ссылка ]

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

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