Mizar Mathematical Library (MML) von Mizar Artikel Zusammensetzung: Die folgenden beiden Artikel bilden die Grundlage dieses Datensatzes.

• eingebaute Begriffe
• die Axiome der Tarski-Grothendieck-Mengenlehre

Die Mizar Mathematical Library (MML) ist eine auf der Sprache Mizar basierende Bibliothek für mathematische Formalismen, die über viele Jahre von vielen Autoren und Betreuern erstellt wurde. Die Mizar-Sprache ist eine computerlesbare Sprache zur Beschreibung mathematischer Theoreme, Beweise und verwandter Konzepte. Die Mizar Math Library enthält formalisierte mathematische Theoreme und Beweise aus einem breiten Spektrum mathematischer Bereiche, darunter Logik, Algebra, Analysis, Geometrie usw. Ziel dieser Bibliothek ist es, eine solide mathematische Grundlage für automatisierte Theorembeweise und formale Argumentation zu bieten. Bisher hat das Mizar-Sprachsystem eine riesige Mizar-Mathematical Library gebildet, die eine gute Grundlage für zukünftige Diskussionen über Mathematik und verwandte Themen gelegt hat.