| dbo:abstract
|
- 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. Fin 2020, 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 troisième après HOL Light et Isabelle, mais devant Coq, 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 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. Fin 2020, 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 troisième après HOL Light et Isabelle, mais devant Coq, 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)
|
| rdfs:comment
|
- 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 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)
|
