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

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

Большинство компьютерных доказательств на сегодняшний день представляют собой реализацию больших доказательств путем исчерпания математической теоремы . Идея состоит в том, чтобы использовать компьютерную программу для выполнения длительных вычислений и предоставить доказательство того, что результат этих вычислений следует данной теореме. В 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 г.