Metamath (Metamath)
| Metamath | |
|---|---|
 | |
| Тип | сайт и инструмент интерактивного доказательства теорем |
| Разработчик | Норман Мегилл (Norman Megill) |
| Написана на | ANSI C |
| Операционные системы | Linux, Windows, macOS |
| Последняя версия | |
| Репозиторий |
github.com/metamath/meta… github.com/metamath/set.… |
| Лицензия | GNU General Public License (Creative Commons Public Domain Dedication for databases) |
| Сайт | metamath.org github.com/metamath/metamath-exe |
Metamath (рус. Метамат; происходит от «metavariable math»[2], рус. «математика с метапеременными») — очень простой формальный язык и соответствующая ему компактная компьютерная программа (инструмент интерактивного доказательства теорем) для формализации, коллекционирования в архиве соответствующего сайта, подтверждения и изучения математических доказательств[3]. Существует несколько баз данных доказанных теорем, разработанных используя Metamath, начиная с классических результатов в логике, теории множеств, теории чисел, алгебре, топологии, анализе и других разделах математики.[4] Данный проект первый в своём роде, который позволяет удобно и интерактивно исследовать свою базу данных формализированных теорем в формате обыкновенного сайта.[5]
По состоянию на июнь 2022 года, собрание всех теорем, доказанных с использованием Metamath насчитывает более 23 000 доказательств[6] и является одним из самых больших в мире формализированной математики. В частности, это собрание включает в себя доказательства 74[7] из 100 теорем из челленджа «Formalizing 100 Theorems» («Формализация 100 теорем»), ставя его на третье место после HOL Light и Isabelle, но перед Coq, Mizar, ProofPower, Lean, Nqthm, ACL2 и Nuprl. Существует по крайней мере 17 инструментов интерактивного доказательства теорем, использующих формат Metamath.[8]
См. также
[править | править код]Примечания
[править | править код]- ↑ Release 0.198 — 2021.
- ↑ Home Page - Metamath. Дата обращения: 14 декабря 2020. Архивировано 24 ноября 2020 года.
- ↑ Megill, Norman. Metamath: A Computer Language for Mathematical Proofs / Norman Megill, David A. Wheeler. — Second. — Morrisville, North Carolina, US : Lulul Press, 2019-06-02. — P. 248. — ISBN 978-0-359-70223-7. Архивная копия от 24 ноября 2020 на Wayback Machine Источник. Дата обращения: 14 декабря 2020. Архивировано 24 ноября 2020 года.
- ↑ Megill, Norman. What is Metamath? Metamath Home Page. Дата обращения: 14 декабря 2020. Архивировано 24 ноября 2020 года.
- ↑ TOC of Theorem List - Metamath Proof Explorer. Дата обращения: 28 февраля 2021. Архивировано 27 июня 2021 года.
- ↑ Home Page - Metamath. Дата обращения: 25 декабря 2020. Архивировано 9 ноября 2020 года.
- ↑ Metamath 100. Дата обращения: 14 декабря 2020. Архивировано 4 февраля 2021 года.
- ↑ Known Metamath proof verifiers. Дата обращения: 14 июля 2019. Архивировано 11 ноября 2020 года.
Ссылки
[править | править код]- Metamath: официальный сайт.
- Source code for the Metamath executable: репозиторий на GitHub.
- What do mathematicians think of Metamath: мнения о Metamath.