Dystrybucja Mizara zawiera Mizar Mathematical Library (MML), bibliotekę zawierającą definicje, twierdzenia i dowody matematyczne do których odwołują się nowe artykuły. Propozycje na dodatki do tej biblioteki, po recenzji i automatycznym sprawdzeniu, są publikowane w Journal of Formalized Mathematics i stają się częścią MML.
MML jest zbudowane w oparciu o aksjomaty teorii mnogości Tarskiego-Grothendiecka. Do chwili obecnej (kwiecień 2006) w bibliotece znalazło się 7900 definicji i 42 000 twierdzeń.
Mimo iż semantycznie wszystkie obiekty MML są zbiorami, język pozwala na definiowanie i używanie nowych typów składniowych: np. zmienna może być zdefiniowana jako Nat, jeśli oznacza liczbę naturalną, albo Group, jeśli oznacza grupę. Sprawia to, że notacja staje się wygodniejsza i bardziej zbliżona do matematycznego sensu danego zapisu.
Abstrakty MML można przeglądać w Journal of Formalized Mathematics, a MML Query implementuje wyszukiwarkę MML.
Przypisy