Metamath (; происходит от «metavariable math», рус. «математика с метапеременными») — очень простой формальный язык и соответствующая ему компактная компьютерная программа (инструмент интерактивного доказательства теорем) для формализации, коллекционирования в архиве соответствующего сайта, подтверждения и изучения математических доказательств . Существует несколько баз данных доказанных теорем, разработанных используя Metamath, начиная с классических результатов в логике, теории множеств, теории чисел, алгебре, топологии, анализе и других разделах математики. Данный проект первый в своём роде, который позволяет удобно и интерактивно исследовать свою базу данных формализированных теорем в формате обыкновенного сайта.
По состоянию на июнь 2022 года, собрание всех теорем, доказанных с использованием Metamath насчитывает более 23 000 доказательств и является одним из самых больших в мире формализированной математики. В частности, это собрание включает в себя доказательства 74 из 100 теорем из челленджа «Formalizing 100 Theorems» («Формализация 100 теорем»), ставя его на третье место после HOL Light и Isabelle, но перед Coq, Mizar, ProofPower, Lean, Nqthm, ACL2 и Nuprl. Существует по крайней мере 17 инструментов интерактивного доказательства теорем, использующих формат Metamath.
См. также Инструмент интерактивного доказательства теорем
Примечания
Ссылки Metamath: официальный сайт. Source code for the Metamath executable: репозиторий на GitHub. What do mathematicians think of Metamath: мнения о Metamath.
Категория:Инструменты интерактивного доказательства теорем Категория:Свободное математическое программное обеспечение