Ensemble De Données Mathématiques Mizar
Date
URL de publication
Licence
CC BY 4.0
Catégories
Bibliothèque mathématique Mizar (MML) par Articles de Mizar Composition, Les deux articles suivants constituent la base de cet ensemble de données.
La bibliothèque mathématique Mizar (MML) est une bibliothèque de formalisme mathématique basée sur le langage Mizar, qui a été construite au fil de nombreuses années par de nombreux auteurs et mainteneurs. Le langage Mizar est un langage lisible par ordinateur permettant de décrire des théorèmes mathématiques, des preuves et des concepts connexes. La bibliothèque mathématique Mizar contient des théorèmes et des preuves mathématiques formalisés couvrant un large éventail de domaines mathématiques, notamment la logique, l'algèbre, l'analyse, la géométrie, etc. L'objectif de cette bibliothèque est de fournir une base mathématique solide pour la preuve automatisée de théorèmes et le raisonnement formel. Jusqu’à présent, le système linguistique Mizar a constitué une immense bibliothèque mathématique Mizar, qui a posé de bonnes bases pour les discussions futures sur les mathématiques et les questions connexes.