Есть ли хранилище для иерархии доказательств?

15

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

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

Я мысленно представляю график, возможно DAG , всех известных математических доказательств, которые можно выразить с помощью английских утверждений, а не доказательств с использованием рисунков . Это будет основная карта (карта в смысле начала в одной точке и перемещения в другую точку через промежуточные точки), а для конкретного помощника по проверке у каждого будет подграф основной карты. Затем, если кто-то хотел создать доказательство, используя помощника по доказательствам, найденного у мастера, а не на подграфе, сравнивая два графика, можно было бы получить представление о работе, необходимой для создания недостающих доказательств для помощника по доказательствам.

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

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

РЕДАКТИРОВАТЬ

В поиске я нашел нечто похожее для математических функций . Я не нашел один для доказательств в NIST

Гай Кодер
источник
1
Вы ищете хранилище кода (для упомянутых систем доказательств) или «хранилище» общих доказательств (написанных на английском языке / математическая запись)? Если последнее, вы видели: proofwiki.org/wiki/Main_Page
Николас Манкузо
Я был бы удивлен, найдя структурированное, всеобъемлющее хранилище доказательств. Кроме того, каждая книга по математике одна.
Рафаэль
1
@NicholasMancuso выглядит многообещающе. Предложение «from» в определениях доказательства, кажется, дает мне то, что мне нужно. Я знаю, что список невелик ~ 5000, но для начинающих мне может хватить карты, чтобы начать. Сделайте ответ, и я проголосую.
Парень Кодер
1
Я не уверен, что такой граф существует - в математике есть утверждения, которые не обязательно следуют непосредственно из ряда других доказательств. Многие геометрические аргументы попадают в эту категорию. Может быть возможно заполнить их, но могут быть моменты, когда никто не удосужился доказать «очевидное». Если бы такой граф существовал, я думаю, он был бы действительно массивным, как по размеру, так и по глубине. Я не могу представить количество шагов, чтобы перейти от ZFC к квадратной формуле, и тем более последней теоремы Ферма.
SamM

Ответы:

11

Система Mizar - это огромное хранилище математических доказательств. Смотрите страницу википедии и официальный сайт .

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

Из википедии / Mizar_system # Mizar_language :

Отличительной чертой языка Mizar является его читабельность

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

Реал Слав
источник
Я знал о библиотеке Mizar, но не знал о графике. Я вызывающе посмотрю на это, когда у меня будет шанс.
Парень кодер
9

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

Николас Манкузо
источник
8

Метамат имеет большой выбор доказательств, построенных прямо из их ядра в логике высказываний.

Тем не менее, это ужасно не хватает с точки зрения теории CS. Не стесняйтесь расширять это!

jmite
источник
Я бросил быстрый взгляд, это выглядит многообещающе.
Гай Кодер
4

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

Обратите внимание, что в области АТМ, автоматического доказательства теорем и вспомогательного доказательства теорем доказательства являются символическими, и на самом деле не представляется возможным или правдоподобным изучать «доказательства на английском языке», как вы визуализируете.

Однако вы можете узнать о парадоксе Ричарда, который начинался как формулировка языка, а затем был символически оформлен. Говорят, что это было источником вдохновения для «сурьмы» (противоречий), обнаруженных в ранней теории множеств, которая исторически даже проложила путь к теореме Гёделя о неполноте.

ВЗН
источник