Interested Article - Metamath

Metamath ( рус. Метамат ; происходит от « meta variable math » , рус. «математика с метапеременными») — очень простой формальный язык и соответствующая ему компактная компьютерная программа ( инструмент интерактивного доказательства теорем ) для формализации, коллекционирования в архиве соответствующего сайта, подтверждения и изучения математических доказательств . Существует несколько баз данных доказанных теорем, разработанных используя Metamath, начиная с классических результатов в логике , теории множеств , теории чисел , алгебре , топологии , анализе и других разделах математики. Данный проект первый в своём роде, который позволяет удобно и интерактивно исследовать свою базу данных формализированных теорем в формате обыкновенного сайта.

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

См. также

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

Примечания

— 2021.
. Дата обращения: 14 декабря 2020. 24 ноября 2020 года.
Megill, Norman. / 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. Metamath Home Page . Дата обращения: 14 декабря 2020. 24 ноября 2020 года.
. Дата обращения: 28 февраля 2021. 27 июня 2021 года.
. Дата обращения: 25 декабря 2020. 9 ноября 2020 года.
Дата обращения: 14 декабря 2020. 4 февраля 2021 года.
. Дата обращения: 14 июля 2019. 11 ноября 2020 года.