Parallelizing Mizar

TL;DR

This paper explores the parallelization of the Mizar proof checking system by leveraging its multi-pass architecture to improve processing efficiency through parallel execution of independent tasks.

Contribution

It introduces a novel method for parallelizing Mizar's proof checking by dividing formalizations into parts processed concurrently, enhancing performance.

Findings

Parallelization improves proof checking speed on large formalizations.

Implementation successfully processes Mizar library examples in parallel.

Future extensions could further optimize the approach.

Abstract

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.