Почему компьютеры не проверяют корректность доказательств математических теорем?

Как раз проверяют. И последние открытия в математике так и сделаны - доказано компьютером, проверено компьютером - и НИКТО на самом деле не знает, в чём суть доказательства и верно ли оно.

Да, я в 8 классе тоже у учителя физики это спрашивал.

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

Да и вообще если бы было такое универсальное средство, нам бы про него наверняка рассказали бы. Штука то интересная.

И что он тебе рассказал?

Сказал «Классная идея!». На этом и всё. Но это было давно, он мог о таком ещё ничего не знать.

Видимо универсального как раз нет. Не знаю почему. Я не разбираюсь в современной математике, там ад какой-то творится.

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

Великая теорема Ферма была доказана именно так.

С разморозкой!

http://en.wikipedia.org/wiki/Automated_theorem_proving
</Thread> (?)

Автоматическое доказательство теорем это другое. Меня интересует автоматическая проверка уже полученного доказательства (неважно каким путём).

Я не разбираюсь в современной математике

Из того, что я видел в универе

Мне кажется, что можно построить некий DSL

Я не разбираюсь в медицине, но из того, что я видел в поликлинике, я сделал вывод, можно изобрести такую таблетку...

Именно это и делает АДТ. Описываешь аксиоматику, ставишь теорему в виде заключения.
Если формальная система сводится к логике первого порядка, то можешь легко проверить истинность заключительного высказывания (проверяемой теоремы) с помощью языка Prolog.

man Обратный логический вывод

Я примерно представляю, как это должно работать. Меня интересует вопрос - почему уважаемый китайский ученый не представил свое доказательство в формально-верифицируемом виде (пролог-программы?). Ну и то же ко всем остальным современным теоремам.

Существует подмножество математики, которое не формализуется логикой первого порядка. Т.н. неаксиоматизируемые теории.

А еще есть «Теорема Гёделя о неполноте»

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

Agda, Coq, AXIOM </thread>

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

Если доказательство теоремы не формализуется логикой, это не теорема, а проповедь.

Coq:

http://en.wikipedia.org/wiki/Four_color_theorem

http://en.wikipedia.org/wiki/Feit–Thompson_theorem

http://math-classes.org

http://corn.cs.ru.nl

http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath

http://r6.ca/Goedel/goedel1.html

http://coq.inria.fr/cocorico/Top100MathematicalTheoremsInCoq

Coq, Agda: http://homotopytypetheory.org

Agda: http://github.com/copumpkin/categories, например.

Для прочих автоматических и ручных систем тоже можно результатов найти — простые теоремы на уровне упражнений (тыщи их), истории успеха — уже по-разному.

Тогда все поймут что эти все умные дядьки попросту дармоеды.

Кстати, вещи типа ассоциативности сложения даже на хаскеле доказываются :)

Вообще-то проверяют, по мере возможности.

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

не формализуется логикой

Какой логикой? Исчеслением высказываний или предикатов? А есть еще логика высшего порядка. Вы разделяете человеческий язык (на быт. «логику») и формальную логику?
Короче, АДТ имеет ограниченное применение.

теорема о неполноте вроде говорит что нельзя создать универсальный математический язык или что-то типа того.

поэтому никто и не пытается.

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

Наверно он имеет ввиду множество натуральных чисел не определяя его как полугруппу.

Сложения на какой алгебраической структуре?

На натуральных числах в аксиоматике Пеано. Или в ZF с общепринятым кодированием чисел множествами и арифметическими функциями на них. Или в теории типов с типами и функциями, соответственно. Или в элементарном топосе. После этого тот факт что <N, +, *, 0, 1> это коммутативное полукольцо, например (включая лемму об ассоциативности +), доказывается как теорема.

Короче, этот факт с точки зрения оснований есть теорема. Конечно, может быть теория где это аксиома (теория моноида, например, да), но в более универсальном базисе это не так.

Или формально: http://darcsden.com/abel/AgdaPrelude/browse/src/Data/Nat/Properties.agda.

Но раз так не делают - видимо я где то ошибаюсь. Хотелось бы знать - где.
... вроде бы процесс проверки доказательства довольно формальный и алгоритмизируемый

Как насчет запостить тут формализацию и алгоритм?

Как раз проверяют. И последние открытия в математике так и сделаны - доказано компьютером, проверено компьютером -

и НИКТО на самом деле не знает, в чём суть доказательства и верно ли оно.

че ты за херню порешь?

Ещё обзор по теме — http://www.ams.org/notices/200811/tx081101370p.pdf.

И последние открытия в математике так и сделаны - доказано компьютером, проверено компьютером

Пруфы будут? Или как обычно.

Великая теорема Ферма была доказана именно так.

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

Тред не читай, сразу отвечай?
Почему компьютеры не проверяют корректность доказательств математических теорем? (комментарий)

Теорема о четырех красках:

The four color theorem was proven in 1976 by Kenneth Appel and Wolfgang Haken. It was the first major theorem to be proved using a computer. Appel and Haken's approach started by showing that there is a particular set of 1,936 maps, each of which cannot be part of a smallest-sized counterexample to the four color theorem. Appel and Haken used a special-purpose computer program to confirm that each of these maps had this property.

А теперь сравним с тем, что сказал ты:

И последние открытия в математике так и сделаны - доказано компьютером

Если проверку 1,936 карт на какое-то свойство считать компьютерным доказательством «для всех карт», то это явный перегиб.

http://www.vokrugsveta.ru/vs/article/7673/

Доказательство, поданное Хейлзом для публикации в авторитетном журнале «Анналы математики», включало 250 страниц записей и около 3 гигабайт компьютерного кода. Для того чтобы осуществить проверку работы Хейлза, журнал созвал комиссию из 20 лучших специалистов в этой области. Комиссия продолжала свою работу до 2004 года (шесть лет!), лишившись за это время большей части своих членов. В итоге было принято решение опубликовать в журнале теоретическую часть работы, а проверку компьютерной части отложить до лучших времен. На сегодняшний день большая часть алгоритмов Хейлза проверена и задача об упаковке шаров считается «решенной на 99%».

Оно там скорее в режиме киборга, а не ИИ :) То есть как вспомогательные средства — сделать полностью формальное доказательство сложнее и муторнее чем неформальное (как у Бурбаки — неформально всегда есть возможность выбрать когда остановиться в формализации, при общении с полностью формальной системой такой возможности нет — вся интуиция должна переводиться в синтаксическую форму полностью), формализация проводится либо постфактум годы после, либо постфактум хотя бы относительно обычной математической интуиции. «Режим ИИ», то есть перечисление всех утверждений с автоматическим поиском подходящих доказательств при их истинности (Entscheidungsproblem), это как раз невозможно для всех достаточно логически богатых теорий (отсюда же следует одна из причин по которой в большей степени предполагается, что P != NP).

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

Но я пошёл дальше и нашёл http://en.wikipedia.org/wiki/Kepler_conjecture#Hales.27_proof
Что ещё интересней, так это следующий раздел http://en.wikipedia.org/wiki/Kepler_conjecture#A_formal_proof

Hales estimates that producing a complete formal proof will take around 20 years of work.

Но я пошёл дальше и нашёл

Это прекрасно. Ко мне вопросы ещё есть?

man проблема остановки и иже с ней

Я вижу две проблемы здесь:

- нету хорошей компьютерной формализации уже доказанных теорем от которых в своих доказательствах отталкиваются доказатели

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