| dbo:abstract
|
- Metamath ist zum einen eine Programmiersprache, die formale Systeme und in solchen Systemen geführte Beweise beschreiben kann, zum anderen ein Online-Archiv von formalen Beweisen, die mit der Metamath-Programmiersprache geführt worden sind. Anders als die üblich in der Mathematik verwendeten informellen Beweise, kann mit Metamath jeder einzelne logische Schritt eines Beweises auf elementare Manipulation von Zeichenketten reduziert werden. (de)
- Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others. As of February 2022, the set of proved theorems using Metamath is one of the largest bodies of formalized mathematics, containing in particular proofs of 74 of the 100 theorems of the "Formalizing 100 Theorems" challenge, making it fourth after HOL Light, Isabelle, and Coq, but before Mizar, , Lean, Nqthm, ACL2, and Nuprl. There are at least 19 proof verifiers for databases that use the Metamath format. This project is the first one of its kind that allows for interactive browsing of its formalized theorems database in the form of an ordinary website. (en)
- Metamath est un langage formel et un logiciel associé (un assistant de preuve) pour rassembler, vérifier et étudier les preuves de théorèmes mathématiques. Plusieurs bases de théorèmes avec leurs preuves ont été développés avec Metamath. Elles rassemblent des résultats standards en logique, théorie des ensembles, théorie des nombres, algèbre, topologie, analyse, entre autres domaines. Début 2022, les théorèmes prouvées à l'aide de Metamath forment l'un des plus grands corps de mathématiques formalisées, et incluent notamment 74 des 100 théorèmes du défi "Formalizing 100 Theorems", ce qui en fait le quatrième après HOL Light et Isabelle et Coq, mais devant , Mizar, Proof Power, Lean, Nqthm, ACL2, et Nuprl. Il y a au moins 17 vérificateurs de preuves pour les bases de théorèmes au format Metamath. Ce projet est le premier de son genre qui permet la navigation interactive d'une base de théorèmes formalisés sous la forme d'un site web. (fr)
- Metamath (рус. Метамат; происходит от «metavariable math», рус. «математика с метапеременными») — очень простой формальный язык и соответствующая ему компактная компьютерная программа (инструмент интерактивного доказательства теорем) для формализации, коллекционирования в архиве соответствующего сайта, подтверждения и изучения математических доказательств. Существует несколько баз данных доказанных теорем, разработанных используя Metamath, начиная с классических результатов в логике, теории множеств, теории чисел, алгебре, топологии, анализе и других разделах математики. Данный проект первый в своём роде, который позволяет удобно и интерактивно исследовать свою базу данных формализированных теорем в формате обыкновенного сайта. По состоянию на июнь 2022 года, собрание всех теорем, доказанных с использованием Metamath насчитывает более 23 000 доказательств и является одним из самых больших в мире формализированной математики. В частности, это собрание включает в себя доказательства 74 из 100 теорем из челленджа «Formalizing 100 Theorems» («Формализация 100 теорем»), ставя его на третье место после HOL Light и Isabelle, но перед Coq, Mizar, , Lean, Nqthm, и . Существует по крайней мере 17 инструментов интерактивного доказательства теорем, использующих формат Metamath. (ru)
- Metamath是用來發展嚴格形式化數學定義及證明的一款語言，亦指用來驗證該語言的，以及存有邏輯、集合論、數論、群論、代數、數學分析、拓撲學、希爾伯特空間及等領域中數萬條已證明定理且仍不斷在增加中的資料庫。 (zh)
|
| rdfs:comment
|
- Metamath ist zum einen eine Programmiersprache, die formale Systeme und in solchen Systemen geführte Beweise beschreiben kann, zum anderen ein Online-Archiv von formalen Beweisen, die mit der Metamath-Programmiersprache geführt worden sind. Anders als die üblich in der Mathematik verwendeten informellen Beweise, kann mit Metamath jeder einzelne logische Schritt eines Beweises auf elementare Manipulation von Zeichenketten reduziert werden. (de)
- Metamath是用來發展嚴格形式化數學定義及證明的一款語言，亦指用來驗證該語言的，以及存有邏輯、集合論、數論、群論、代數、數學分析、拓撲學、希爾伯特空間及等領域中數萬條已證明定理且仍不斷在增加中的資料庫。 (zh)
- Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others. This project is the first one of its kind that allows for interactive browsing of its formalized theorems database in the form of an ordinary website. (en)
- Metamath est un langage formel et un logiciel associé (un assistant de preuve) pour rassembler, vérifier et étudier les preuves de théorèmes mathématiques. Plusieurs bases de théorèmes avec leurs preuves ont été développés avec Metamath. Elles rassemblent des résultats standards en logique, théorie des ensembles, théorie des nombres, algèbre, topologie, analyse, entre autres domaines. Ce projet est le premier de son genre qui permet la navigation interactive d'une base de théorèmes formalisés sous la forme d'un site web. (fr)
- Metamath (рус. Метамат; происходит от «metavariable math», рус. «математика с метапеременными») — очень простой формальный язык и соответствующая ему компактная компьютерная программа (инструмент интерактивного доказательства теорем) для формализации, коллекционирования в архиве соответствующего сайта, подтверждения и изучения математических доказательств. Существует несколько баз данных доказанных теорем, разработанных используя Metamath, начиная с классических результатов в логике, теории множеств, теории чисел, алгебре, топологии, анализе и других разделах математики. Данный проект первый в своём роде, который позволяет удобно и интерактивно исследовать свою базу данных формализированных теорем в формате обыкновенного сайта. (ru)
|
