  This paper surveys and describes the implementation of parallelization of the
Mizar proof checking and of related Mizar utilities. The implementation makes
use of Mizar's compiler-like division into several relatively independent
passes, with typically quite different processing speeds. The information
produced in earlier (typically much faster) passes can be used to parallelize
the later (typically much slower) passes. The parallelization now works by
splitting the formalization into a suitable number of pieces that are processed
in parallel, assembling from them together the required results. The
implementation is evaluated on examples from the Mizar library, and future
extensions are discussed.
