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]

См. также

[править | править код]

Примечания

[править | править код]
  1. ↑ Release 0.198 — 2021.
  2. ↑ Home Page - Metamath. Дата обращения: 14 декабря 2020. Архивировано 24 ноября 2020 года.
  3. ↑ 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 года.
  4. ↑ Megill, Norman. What is Metamath? Metamath Home Page. Дата обращения: 14 декабря 2020. Архивировано 24 ноября 2020 года.
  5. ↑ TOC of Theorem List - Metamath Proof Explorer. Дата обращения: 28 февраля 2021. Архивировано 27 июня 2021 года.
  6. ↑ Home Page - Metamath. Дата обращения: 25 декабря 2020. Архивировано 9 ноября 2020 года.
  7. ↑ Metamath 100. Дата обращения: 14 декабря 2020. Архивировано 4 февраля 2021 года.
  8. ↑ Known Metamath proof verifiers. Дата обращения: 14 июля 2019. Архивировано 11 ноября 2020 года.

Ссылки

[править | править код]