Metamath

Metamath (рус. Метамат; происходит от «metavariable math»[2], рус. «математика с метапеременными»…

Metamath
Metamath
Тип сайт, инструмент интерактивного доказательства теорем, proof language[вд] и proof verifier[вд]
Разработчик Норман Мегилл (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 года.

Ссылки

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.