Metamath

Metamath (рус. Метамат; происходит от «metavariable mathematics», рус. «математика с метапеременными») — очень простой формальный язык и соответствующая ему компактная компьютерная программа (инструмент интерактивного доказательства теорем) для коллекционирования в архиве соответствующего сайта, подтверждения и изучения математических доказательств[2]. Несколько баз данных доказанных теорем были разработаны используя Metamath, начиная со стандартных результатов в логике, теории множеств, теории чисел, алгебры, топологии, анализа и других разделах математики.[3] Данный проект первый в своём роде, который позволяет интерактивно исследовать свою базу данных формализированных теорем в формате обыкновенного сайта.[4]

Metamath
Тип сайт
Разработчик Норман Мегилл (Norman Megill)
Написана на ANSI C
Операционная система Linux, Windows, macOS
Последняя версия
Лицензия GNU General Public License (Creative Commons Public Domain Dedication for databases)
Сайт metamath.org

По состоянию на февраль 2021 года, собрание всех доказанных теорем с использованием Metamath насчитывает более 23 000 доказательств[5] и является одним из самых больших в мире формализированной математики. В частности, это собрание включает в себя доказательства 74[6] из 100 теорем из челленджа «Formalizing 100 Theorems» («Формализация 100 теорем»), ставя его на третье место после HOL Light и Isabelle, но перед Coq, Mizar, ProofPower, Lean, Nqthm, ACL2 и Nuprl. Существует по крайней мере 17 инструментов интерактивного доказательства теорем, использующих формат Metamath.[7]

См. также

Примечания
  1. Release 0.196 — 2021.
  2. 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.
  3. Megill, Norman. What is Metamath?. Metamath Home Page.
  4. TOC of Theorem List - Metamath Proof Explorer
  5. Home Page - Metamath
  6. Metamath 100.
  7. Known Metamath proof verifiers. Дата обращения: 14 июля 2019.

Ссылки
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.