Mizar ,a proof-checking system,is used to build the Mizar Mathematical Library (MML ).This is a long term project aiming at
building a comprehensive library of mathematical knowledge. The language and the checking software evolve, and the evolution
is driven by the growing library. We discuss the issues of maintaining integrity of an electronic repository of formal mathematics,
based on our experience with MML .
Partially supported by NSERC grant OGP9207.
Partially supported by FP5 grant HPRN-CT-2000-00102.