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

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

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

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

Методы

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

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

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

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

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

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

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

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

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

Приложения

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

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

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

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

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

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

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

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