All other texts undergo verification by Mizar
to be correct consequences of those axioms.
The Mizar system
assists the author of a new text in preparing
available terminology and results, verifies the claims of the text and
extracts facts and definitions for inclusion into the library.
The task of building a rich mathematical library is
currently the main effort of the Mizar community.
Most of the library texts formalize the fundamentals of introductory
mathematics. Some of the texts contribute more advanced results.