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

[fractalon]

Существуют ли языки типа языков программирования (с соответствующими компиляторами), позволяющие формально записать доказательство как последовательность выводов, использовать уже выведенные утверждения, составлять что-то вроде программистских библиотек?
То есть такой язык, на котором можно было бы более-менее удобно записать доказательство и автоматически проверить? Как в учебниках по логике приводят "4=ModusPonenus(2,3)". Понятно, что формальные доказательства всегда ужасно длинные (и единица от Бурбаки, и всё такое...), но ведь можно, наверное, выделить те шаблоны, те очевидные утверждения, которыми мы пользуемся (их, может, много, но конечно), вынести их в отдельный файл такого языка и просто подключать. И потом наращивать аппарат доказательств...

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

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

[Dan B-Yallay]

Пролог?

[Someone]

https://ru.wikipedia.org/wiki/Coq

[fractalon]

Dan B-Yallay
Пролог, насколько я его мельком видел, всё-таки всегда решает какую-то задачу, вычисляет. Ну, если угодно, ищет доказательства. А я говорю о том, чтоб не программа искала доказательство, а сама программа была доказательством и в дальнейшем анализе/переборе/вычислении не нуждалась.

[Someone]

Непонятно тогда, чего Вы хотите.
Берите язык формальной математической логики, пополняйте его необходимыми элементами и пишите себе.

[fractalon]

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

[Karan]

Есть много таких языков, например, Coq, Agda, Mizar, Isabelle, Lean.

[Sender]

MetaMath ещё. Вообще, на этой страничке перечислено некоторое количество таких систем. Их можно найти, например, в категориях "proof checker" и "prover".

[whitefox]

Упомяну ещё интересный российский проект языка Russell на основе Metamath.

Кстати, проект Mizar издаёт журнал Formalized Mathematics в котором публикуются доказательства проверенные этой системой.

[arseniiv]

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

[NO.]

В любой системе с логикой высших порядков (HOL) можно определять новые понятия, их семантику, грамматику выражений, правила логики и тактики доказательств, потом все это выполнять. Хоть в JavaScript можно. Есть российский Refal, тоже работа с символами. Во всех математических пакетах есть средства символьной алгебры, хотя бы скобочки раскрывать, да выразить x через y где всё обращается. В metamath есть большой файл с теоремами, там вроде по Бурбаки много математики выстроено, любопытно посмотреть как практически с нуля всё начинается. Но там только верификация уже имеющихся доказательств. Про креатив есть работы по доказательству в HOL средствами логики первого порядка, строятся какие-то счетные множества теорем. Проблема как из всбесившегося принтера выловить практически ценные теоремы. Над всем довлеет проблема неразрешимости, то есть доказано, что в некоторых формальных системах не существует алгоритма доказательства любого выражения.