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

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

См. также

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

Примечания

Ссылки

• : официальный сайт.
• : репозиторий на GitHub.
• : мнения о Metamath.