Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

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

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

Методы [ править ]

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

Философские возражения [ править ]

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

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

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

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

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

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

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

Приложения [ править ]

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

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

  • Теорема четырех цветов , 1976
  • Гипотеза Митчелла Фейгенбаума об универсальности в нелинейной динамике. Доказано О.Э. Лэнфордом с использованием строгой компьютерной арифметики, 1982 г.
  • Connect Four , 1988 - решенная игра
  • Несуществование конечной проективной плоскости порядка 10, 1989 г.
  • Гипотеза о двойном пузыре , 1995 [2]
  • Гипотеза Роббинса , 1996 г.
  • Гипотеза Кеплера , 1998 г. - проблема оптимальной упаковки сфер в коробку.
  • Аттрактор Лоренца , 2002 г. - 14-я проблема Смейла, доказанная Уориком Такером с использованием интервальной арифметики.
  • Случай из 17 пунктов проблемы счастливого конца , 2006 г.
  • NP-твердость по минимальной весовой триангуляции , 2008
  • Оптимальные решения для кубика Рубика можно получить не более чем за 20 ходов лицом, 2010 г.
  • Минимальное количество подсказок для решаемой головоломки Судоку - 17, 2012 г.
  • В 2014 году частный случай проблемы несоответствия Эрдеша был решен с помощью SAT-решателя . Полное предположение позже было решено Теренсом Тао без помощи компьютера. [3]
  • Задача логических троек Пифагора решена с использованием 200 терабайт данных в мае 2016 г. [4]
  • Приложения к теории Колмогорова-Арнольда-Мозера [5] [6]
  • Свойство Каждана (T) для группы автоморфизмов свободной группы ранга не менее пяти

Теоремы на продажу [ править ]

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

См. Также [ править ]

  • Подтвержденные числа
  • Математическое доказательство
  • Проверка модели
  • Проверка доказательств
  • Символьное вычисление
  • Автоматизированное рассуждение
  • Формальная проверка
  • Семнадцать или бюст
  • Метамат

Ссылки [ править ]

  1. ^ Tymoczko, Томас (1979), "Четыре-Color Проблема и ее математический смысл", Журнал философии , 76 (2): 57-83, DOI : 10,2307 / 2025976 , JSTOR  2025976.
  2. Перейти ↑ Hass, J., Hutchings, M., & Schlafly, R. (1995). Гипотеза о двойном пузыре. Объявления об электронных исследованиях Американского математического общества, 1 (3), 98-102.
  3. ^ Чезаре, Крис (1 октября 2015 г.). «Математик разгадывает загадку мастера» . Природа . 526 (7571): 19–20. Bibcode : 2015Natur.526 ... 19С . DOI : 10.1038 / nature.2015.18441 . PMID 26432222 . 
  4. ↑ Лэмб, Эвелин (26 мая 2016 г.). «Математическое доказательство в двести терабайт - самое большое доказательство за всю историю» . Природа . 534 (7605): 17–18. Bibcode : 2016Natur.534 ... 17L . DOI : 10.1038 / nature.2016.19990 . PMID 27251254 . 
  5. ^ Celletti, А., & Chierchia, Л. (1987). Строгие оценки компьютерной теории КАМ. Журнал математической физики, 28 (9), 2078-2086.
  6. Перейти ↑ Figueras, JL, Haro, A., & Luque, A. (2017). Строгое компьютерное применение теории КАМ: современный подход. Основы вычислительной математики, 17 (5), 1123-1193.
  7. ^ "Статья в Herald Gazette о покупке собственной теоремы" . Herald Gazette Scotland . Ноября 2010 Архивировано из оригинала на 2010-11-21.
  8. ^ "Школа информатики, Университет Эдинбурга" . Школа информатики Эдинбургского университета . Апрель 2015 г.[ постоянная мертвая ссылка ]

Дальнейшее чтение [ править ]

  • Lenat, DB, (1976), AM: Подход искусственного интеллекта к открытиям в математике как эвристический поиск , доктор философии. Диссертация, STAN-CS-76-570, и отчет по проекту эвристического программирования HPP-76-8, Стэнфордский университет, лаборатория искусственного интеллекта, Стэнфорд, Калифорния.
  • Мейер, KR, & Schmidt, DS (ред.). (2012). Компьютерные доказательства в анализе. Springer Science & Business Media .
  • М. Накао, М. Плам, Ю. Ватанабэ (2019) Методы численной проверки и компьютерные доказательства для дифференциальных уравнений с частными производными (серии Спрингера в вычислительной математике).

Внешние ссылки [ править ]

  • Оскар Э. Лэнфорд; Компьютерное доказательство гипотез Фейгенбаума , "Bull. Amer. Math. Soc.", 1982 г.
  • Эдмунд Фурс; Почему АМ выдохлась?
  • Цифровые доказательства, сделанные компьютером, могут ошибаться
  • «Специальный выпуск о формальном доказательстве» . Уведомления Американского математического общества . Декабрь 2008 г.