(1.66GHz Intel Atom) takes 2s, while on a recent lower-range server (2 quadcore hyperthreading 2.27GHz Intel Xeons) the same task takes 0.5s. For a more involved article this difference becomes more visible, and can be the deciding factor for the usability and real-time experience with the system. For example, for the more involved Mizar article fdiff 1 9 about real function differentiability
[19], the difference is 23s vs. 6s.

The latest advances in CPU power have been achieved mainly by packing multiple CPUs together, instead of raising the speed of individual CPUs. To take advantage of this, Mizar processing has recently been parallelized10, and the parallel version of the Mizar verifier is running on our server. This (depending on the success of the parallelization) can further significantly improve the real-time verification experience. For example, on the even longer Mizar article fdiff 2 11 about real function differentiability [13], the difference between running the parallel version (using eight cores) and the non-parallel version is a factor of four (31s vs. 7.8s). Verification of this article using the above mentioned notebook takes 125s, resulting in a speed-up factor of sixteen (and substantially improving the real-time interaction with the system).

The last important advantage is that a server-based installation supports use of modified, enhanced, and experimental versions of the verifier. This can provide useful additional functionalities. For instance, the Mizar parallelizer requires additional software to run, and a recently modified version of the Mizar verifier that has not yet been distributed to Mizar users. Translation of Mizar articles to ATP formats also requires a version of the verifier that has been compiled with a special flag, again not included in the standard Mizar distribution. An online service can also easily include multiple versions of the Mizar library and binaries, as is done for the MML Query service [2].

## 3.2 Htmlization Of Mizar Articles

There has been quite a lot of recent work on XMLization and HTMLization of Mizar articles [29, 35], including the addition of useful additional information into the XML form of the Mizar article and its HTML presentation. There are two major reasons for having a static HTMLized MML available:12 (i) to provide fast browsing of the theorems and definitions used in a particular formalization, with a number of user-friendly features (like (sub)proof hiding/showing, etc.), and (ii) providing explanations for a number of phenomena in the formalization that are made explicit and clear only during verification, and are hard to decipher from the formalization text alone. The latter includes, for example:
- Explicit HTML presentation of the current goal (thesis), computed by the verifier at each point of the formalization.

9http://mws.cs.ru.nl/~mptp/mml/mml/fdiff_1.miz 10 The description of the Mizar parallelization and related experiments is unpublished as of January 2010. The parallelizer is available at http://github.com/JUrban/ MPTP2/raw/master/MizAR/cgi-bin/bin/mizp.pl.

11 http://mws.cs.ru.nl/~mptp/mml/mml/fdiff_2.miz 12 It is available at http://mws.cs.ru.nl/~mptp/mml/html/