Bibliothèque mathématique Mizar (MML) par Articles de Mizar Composition, Les deux articles suivants constituent la base de cet ensemble de données.

• notions intégrées
• les axiomes de la théorie des ensembles de Tarski-Grothendieck 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.