Я самообучающийся помощник по доказательствам и решил начать с некоторых базовых доказательств и продолжить работу. Поскольку доказательства основаны на других доказательствах и поэтому образуют иерархию, существует ли хранилище иерархии доказательств?
Я знаю, что могу выбрать конкретного помощника по проверке и проанализировать его библиотеку, чтобы извлечь его иерархию, однако, если я хочу найти следующее доказательство в цепочке доказательств, я не могу, когда его нет в библиотеке.
Я мысленно представляю график, возможно DAG , всех известных математических доказательств, которые можно выразить с помощью английских утверждений, а не доказательств с использованием рисунков . Это будет основная карта (карта в смысле начала в одной точке и перемещения в другую точку через промежуточные точки), а для конкретного помощника по проверке у каждого будет подграф основной карты. Затем, если кто-то хотел создать доказательство, используя помощника по доказательствам, найденного у мастера, а не на подграфе, сравнивая два графика, можно было бы получить представление о работе, необходимой для создания недостающих доказательств для помощника по доказательствам.
Я знаю, что математические доказательства не обязательно легко конвертируемы для использования с помощником по доказательствам, однако общее представление о том, что делать, гораздо лучше, чем вообще ничего.
Также, имея основную карту, я могу видеть, есть ли несколько путей от одной точки до другой, и выбрать путь, который более подходит для конкретного помощника по проверке.
РЕДАКТИРОВАТЬ
В поиске я нашел нечто похожее для математических функций . Я не нашел один для доказательств в NIST
источник
Ответы:
Система Mizar - это огромное хранилище математических доказательств. Смотрите страницу википедии и официальный сайт .
Из википедии / Mizar_system # Mizar_language :
Доказательства написаны в виде статей, из которых более тысячи статей и более 50000 доказанных теорем. На странице википедии упоминаются некоторые интересные идеи « манифеста QED », и о том, как Мицар может достичь этого.
источник
ProofWiki содержит приличное количество доказательств из различных областей математики. Он ни в коем случае не завершен, но является хорошей отправной точкой для того, что вы хотите.
источник
Метамат имеет большой выбор доказательств, построенных прямо из их ядра в логике высказываний.
Тем не менее, это ужасно не хватает с точки зрения теории CS. Не стесняйтесь расширять это!
источник
Смотрите архив TPTP , Тысячи задач для доказателей теорем. Это несколько стандартно в этой области. Это больше «узлы» графа теорем, о которых вы спрашиваете. Некоторые документы, относящиеся к архиву, возможно, исследовали края на этом графике.
Обратите внимание, что в области АТМ, автоматического доказательства теорем и вспомогательного доказательства теорем доказательства являются символическими, и на самом деле не представляется возможным или правдоподобным изучать «доказательства на английском языке», как вы визуализируете.
Однако вы можете узнать о парадоксе Ричарда, который начинался как формулировка языка, а затем был символически оформлен. Говорят, что это было источником вдохновения для «сурьмы» (противоречий), обнаруженных в ранней теории множеств, которая исторически даже проложила путь к теореме Гёделя о неполноте.
источник