Math Proof Verifier

[snyders]

Вполне реально, кажется, создать программу, которая способна проследить правильность доказательства любой теоремы. Вести от простого к более сложному, постепенно накапливая базу "знаний". Пропускать через нее все новые мат. публикации. Никакого супер AI тут вроде не надо, а польза была бы огромная -- искать теоремы, исходя из известных теорем каковы свойства заданного объекта, искать похожие объекты/теоремы, искать обобщения или аналогии между различными областями математики.

Затем можно начинать закладывать простые методы рассуждения: от противного, индукция, двойственность, обобщение, контр-пример etc. Собственно уже в процессе обучения можно классифицировать методы доказательства и пытаться усваивать их. Выдать все теоремы, в доказательстве которых, встречается данный метод рассуждения, данная теорема.
Часто используемые методы теоремы считать фундаментальными (типа theorem-rank).

Comments

[avva.livejournal.com]

На самом деле совершенно нереальная задача.

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

[snyders.livejournal.com]

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

Сразу начать работать со "state of the art" результатами конечно невозможно -- так же как невозможно объяснить ясельнику доказательство теоремы Ферма. Если наращивать базу постепенно от элементарных знаний к более сложным, то машина и будет математиком "знающим" данную область, в том смысле, что все результаты на кот. ссылается новая статья будут уже в базе.

без затраты огромного кол-ва человеческого времени

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

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

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

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

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

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

Простая оценка дает обьем примерно 200-300Гб с ежегодным ростом на 1Гб -- ничего фантастического (10000 математиков в среднем по 2 статьи в год по 50K latex'a = 1Гб в год).

[ex-udod985.livejournal.com]

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

[snyders.livejournal.com]

Если найдется ссылка, киньте мне пожалуйста -- очень интересно.