С развитием математики, усложнением и появлением новых ответвлений, мы наблюдаем очень беспокойные тенденции: из-за слишком «глубокой и специфичной» теории и подходов к доказательству, научное сообщество просто не может проверить многие результаты. Ручная проверка работы сравнялась по сложности с написанием работы. В итоге современная математика наполнена непроверенными теоремами, и это пирамида продолжает расти. Например, в результатах Воеводского, за которые он получил Филдсовскую премию, уже впоследствии были найдены серьезные ошибки, ситуация закончилась благополучно, потому что спустя много лет Воеводский таки смог исправить ошибки - но сам случай симптоматичный. Никто не мог проверить почти 10 лет доказательство abc-гипотезы японским математиком Матидзуки, его док-во на 600 страниц остаётся в подвешенном состоянии до сих пор, не смотря на принятие работы в журнал. Аналогичная проблема была с проверкой доказательство теоремы Ферма на 100 страниц от Эндрю Уайлса.
Как избежать этих проблем? Правильно - автоматизировать и делегировать компьютеру проверку доказательств. Но для этого нужно записывать док-ва в понятном машине формате, для этого и были созданы такие языки формальных верификаций как Lean v4, Agda, Isabelle, Idris, а так же Coq (Воеводский осмыслял его теоретические основания). Если доказательство записано корректно, то система быстро его проверит. Эти системы включают библиотеки, содержащие модули, в них определяются мат концепции, которые переопределяются через другие модули с более базовыми понятиями, получается некоторое вложение абстракций. Актуальная проблема в том, что пакетов и модулей внутри языков для записи доказательств для современной математики на данный момент недостаточно. При этом уже существует множество формализаций известных классических теорем, Фриком Вейдиком отслеживался прогресс в формализации 100 величайших теорем - на данный момент 99% сделано, осталась лишь Великая теорема Ферма.
Ниже пример записи на языке Isabell базовой леммы из геометрии о Сумме углов треугольника. Здесь представлено доказательство этой теоремы из модуля Triangle.
lemma angle_sum_triangle:
assumes "a ≠ b ∨ b ≠ c ∨ a ≠ c"
shows "angle c a b + angle a b c + angle b c a = pi"
ML в настоящий момент даёт новый виток развитию автоматических доказательств. Помимо модели Llemmа, за последние годы появилось много исследований в области пруверов: Например, модель ASTactic обученная на датасете CoqGym, успешно предлагает тактики доказательств в виде абстрактных синтаксических деревьев (AST). Система TRAIL c помощью RL ищет оптимальную стратегию доказательства теорем. GPT-f генерирует доказательства на языке Metamath, а недавняя работа HyperTree Proof Search предлагает модель превосходящую по точности GPT-f и обученную на Lean v4.
