Инструмент интерактивного доказательства теорем

Инструмент интерактивного доказательства теорем (англ. interactive theorem prover, также proof assistant, «помощник в доказательствах») — это программное обеспечение, предназначенное для содействия в построении официальных доказательств с помощью совместной работы человека и машины. Такой инструмент обычно включает в себя некоторый интерактивный редактор доказательств или другой интерфейс, который позволяет пользователю направлять процесс поиска доказательств, детали которых сохраняются на компьютере, при этом отдельные шаги поиска могут выполняться автоматически.

Одним из современных направлений в этой области является внедрение методов искусственного интеллекта, позволяющих автоматизировать формализацию обычной математики^[1].

Название	Последняя версия	Разработчик(и)	Язык реализации	Возможности
Название	Последняя версия	Разработчик(и)	Язык реализации	Высший порядок	Зависимые типы	Малое ядро	Автоматизация доказательств	Доказательство отражением	Генерация кода
ACL2	8.3	Мэтт Кауфман (Matt Kaufmann), Дж. Стротер Мур (J Strother Moore)	Common Lisp	Нет	Безтиповой	Нет	Да	Да	Уже исполняется
Agda	2.6.4.3	Ульф Норелль, Нильс Андерс Даниельссон, Андреас Абель (Chalmers, Гётеборг)	Haskell	Да	Да ^[2]	Да	Нет	Частично	Уже исполняется
Albatross	0.4	Хельмут Брандль	OCaml	Да	Нет	Да	Да	Неизвестно
F*	репозиторий	Microsoft Research и INRIA	F*	Да	Да	Нет	Да	Да	Да
HOL Light	репозиторий	Джон Харрисон	OCaml	Да	Нет	Да	Да	Нет	Нет
HOL4	Kananaskis-13 (или репозиторий)	Майкл Норриш, Конрад Слинд и др.	Standard ML	Да	Нет	Да	Да	Нет	Да
Idris	2 0.6.0	Эдвин Брейди	Idris	Да	Да	Да	Неизвестно	Частично	Да
Isabelle	Isabelle2025 (март 2025)	Ларри Полсон (Cambridge), Тобиас Нипков (Мюнхен), Макариус Венцель	Standard ML, Scala	Да	Нет	Да	Да	Да	Да
Lean	v4.23.0^[3]	Леонардо де Моура (Microsoft Research)	C++, Lean	Да	Да	Да	Да	Да	Да
LEGO	1.3.1	Рэнди Поллак (Эдинбург)	Standard ML	Да	Да	Да	Нет	Нет	Нет
Metamath	v0.198^[4]	Норман Мегилл	ANSI C
Mizar	8.1.11	Университет Белостока	Free Pascal	Частично	Да	Нет	Нет	Нет	Нет
Nqthm
NuPRL	5	Корнеллский университет	Common Lisp	Да	Да	Да	Да	Неизвестно	Да
PVS	6.0	SRI International	Common Lisp	Да	Да	Нет	Да	Нет	Неизвестно
Rocq	9.0	INRIA	OCaml	Да	Да	Да	Да	Да	Да
Twelf	1.7.1	Франк Пфеннинг, Карстен Шурман	Standard ML	Да	Да	Неизвестно	Нет	Нет	Неизвестно

ACL2 — язык программирования, логическая теория первого порядка и инструмент доказательства теорем (имеет как интерактивный, так и автоматический режимы) в традиции Бойера—Мура.
Rocq (прежнее название: Coq) — позволяет формулировать математические утверждения, автоматически проверять их доказательства, строить формальные доказательства и извлекать сертифицированную программу из конструктивного доказательства формальной спецификации.
Семейство HOL — группа систем, изначально происходящих от LCF. Логическое ядро формируется библиотекой их языка программирования. Теоремы — это новые элементы языка, которые могут быть введены только посредством "стратегий", гарантирующих логическую корректность. Составление стратегий позволяет строить большие доказательства с относительно небольшим количеством действий пользователя. К семейству относятся:
- HOL4 — основной "потомок", в активной разработке. Поддержка Moscow ML и Poly/ML. Лицензия BSD.
- HOL Light — "минималистский форк" на базе OCaml.
- ProofPower — был коммерческим, затем вновь стал открытым. Основывается на Standard ML.
IMPS, An Interactive Mathematical Proof System.
Isabelle — интерактивная система доказательства теорем, преемник HOL. Основная кодовая база распространяется по лицензии BSD, но в поставку включено немало дополнительных инструментов с иными лицензиями.
Jape — на языке Java.
Lean
LEGO
Matita — легковесная система на основе исчисления индуктивных конструкций.
MINLOG — интерактивный помощник для минимальной логики первого порядка.
Mizar — на основе логики первого порядка и посылок натурального дедуктивного стиля, а также теории множеств Тарского–Гротендика.
PhoX — инструмент для высокоуровневой логики, расширяемый.
Prototype Verification System (PVS) — средство и язык доказательства, основанный на логике высшего порядка.
Theorem Proving System (TPS) и ETPS — интерактивные инструменты доказательства, также основанные на просто типизированном λ-исчислении, но с независимой реализацией логической теории и кода.

Популярным фронтендом для многих инструментов доказательства является Proof General — расширение на базе Emacs, разработанное в Эдинбургском университете.

Rocq включает RocqIDE, написанный на OCaml с использованием библиотеки Gtk. Isabelle поставляется с Isabelle/jEdit — интерфейсом на основе jEdit и инфраструктуры Scala для документно-ориентированной работы с доказательствами. В последнее время стали появляться расширения для Visual Studio Code для Rocq^[5], Isabelle (разработки Макариуса Венцеля)^[6], и Lean 4 (разработчики leanprover)^[7].

Фрик Вейдейк (Freek Wiedijk) ведёт рейтинг инструментов доказательства по количеству формализованных теорем из списка из 100 известных теорем. На сентябрь 2025 года только шесть систем формализовали более 70 % этих теорем: Isabelle, HOL Light, Lean, Rocq, Metamath и Mizar^[8].

См. также: Компьютерно-поддерживаемое доказательство#Теоремы, доказанные с помощью компьютерных программ

Ниже приводится перечень известных математических результатов, доказанных средствами интерактивных инструментов доказательства.

Теорема	Инструмент	Год
Теорема о четырёх красках	Rocq	2005
Теорема Фейта–Томпсона^[9]	Rocq	2012
Фундаментальная группа окружности^[10]	Rocq	2013
Проблема Эрдёша — Грэма^[11]^[12]	Lean	2022
Конъюнктура Фреймана—Ружсы для $\mathbb {F} _{2}$ ^[13]	Lean	2023
BB(5) = 47 176 870^[14]	Rocq	2024

↑ Ornes, Stephen Quanta Magazine – How Close Are Computers to Automating Mathematical Reasoning? (англ.). Quanta Magazine (27 августа 2020). Дата обращения: 12 апреля 2024.
↑ The Agda Wiki (неопр.). Дата обращения: 31 июля 2024.
↑ Lean 4 Releases Page (неопр.). GitHub. Дата обращения: 22 сентября 2025.
↑ Release v0.198 metamath/Metamath-exe (неопр.). GitHub. Дата обращения: 1 июля 2024.
↑ coq-community/vscoq (неопр.). GitHub (29 июля 2024). Дата обращения: 31 июля 2024.
↑ Wenzel, Makarius Isabelle (неопр.). Дата обращения: 2 ноября 2019.
↑ VS Code Lean 4 (неопр.). GitHub. Дата обращения: 15 октября 2023.
↑ Wiedijk, Freek Formalizing 100 Theorems (неопр.) (22 сентября 2025). Дата обращения: 31 июля 2025.
↑ Feit thomson proved in coq - Microsoft Research Inria Joint Centre (неопр.) (19 ноября 2016). Дата обращения: 7 декабря 2023. Архивировано 19 ноября 2016 года.
↑ Licata, Daniel R. Calculating the Fundamental Group of the Circle in Homotopy Type Theory // 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science / Daniel R. Licata, Michael Shulman. — 2013. — P. 223–232. — ISBN 978-1-4799-0413-6. — doi:10.1109/lics.2013.28.
↑ Math Problem 3,500 Years In The Making Finally Gets A Solution (англ.). IFLScience (11 марта 2022). Дата обращения: 9 февраля 2024.
↑ Avigad, Jeremy (2023), Mathematics and the formal turn, arΧiv:2311.00007 [math.HO].
↑ Sloman, Leila 'A-Team' of Math Proves a Critical Link Between Addition and Sets (англ.). Quanta Magazine (6 декабря 2023). Дата обращения: 7 декабря 2023.
↑ We have proved "BB(5) = 47,176,870" (англ.). The Busy Beaver Challenge (2 июля 2024). Дата обращения: 9 июля 2024.

Pfenning, Frank. The practice of logical frameworks // Trees in Algebra and Programming – CAAP '96. — Springer, 1996. — Vol. 1059. — P. 119–134. — ISBN 3-540-61064-2. — doi:10.1007/3-540-61064-2_33.
Wiedijk, Freek The Seventeen Provers of the World (неопр.). Radboud University Nijmegen (2005). Дата обращения: 10 августа 2023.

Музей инструментов доказательства
«Введение» в Certified Programming with Dependent Types
Введение в Coq Proof Assistant (общий обзор интерактивных помощников доказательства)
Интерактивное доказательство для пользователей Agda
Каталог инструментов для доказательства теорем

Специфические логические фреймворки и реализации (неопр.). Дата обращения: 15 февраля 2024. Архивировано 10 апреля 2022 года. (Фрэнк Пфенн

[1] Ornes, Stephen Quanta Magazine – How Close Are Computers to Automating Mathematical Reasoning? (англ.). Quanta Magazine (27 августа 2020). Дата обращения: 12 апреля 2024.

[agdaWiki-2] The Agda Wiki (неопр.). Дата обращения: 31 июля 2024.

[3] Lean 4 Releases Page (неопр.). GitHub. Дата обращения: 22 сентября 2025.

[4] Release v0.198 metamath/Metamath-exe (неопр.). GitHub. Дата обращения: 1 июля 2024.

[5] q-community/vscoq (неопр.). GitHub (29 июля 2024). Дата обращения: 31 июля 2024.

[6] Wenzel, Makarius Isabelle (неопр.). Дата обращения: 2 ноября 2019.

[7] VS Code Lean 4 (неопр.). GitHub. Дата обращения: 15 октября 2023.

[8] Wiedijk, Freek Formalizing 100 Theorems (неопр.) (22 сентября 2025). Дата обращения: 31 июля 2025.

[9] Feit thomson proved in coq - Microsoft Research Inria Joint Centre (неопр.) (19 ноября 2016). Дата обращения: 7 декабря 2023. Архивировано 19 ноября 2016 года.

[10] Licata, Daniel R. Calculating the Fundamental Group of the Circle in Homotopy Type Theory // 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science / Daniel R. Licata, Michael Shulman. — 2013. — P. 223–232. — ISBN 978-1-4799-0413-6. — doi:10.1109/lics.2013.28.

[11] Math Problem 3,500 Years In The Making Finally Gets A Solution (англ.). IFLScience (11 марта 2022). Дата обращения: 9 февраля 2024.

[12] Avigad, Jeremy (2023), Mathematics and the formal turn, arΧiv:2311.00007 [math.HO].

[13] Sloman, Leila 'A-Team' of Math Proves a Critical Link Between Addition and Sets (англ.). Quanta Magazine (6 декабря 2023). Дата обращения: 7 декабря 2023.

[14] We have proved "BB(5) = 47,176,870" (англ.). The Busy Beaver Challenge (2 июля 2024). Дата обращения: 9 июля 2024.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

Инструмент интерактивного доказательства теорем

Сравнение систем

Пользовательские интерфейсы

Степень формализации математики

Примеры известных формализованных доказательств

Примечания

Литература

Ссылки