information needed for further processing into ATP problems. Like the static HTMLized MML, a static copy of the MML in MPTP format is available to MizAR. It is used for building translated MML items (theorems, definitions, formulae encoding Mizar type automations, etc.) that are necessary for creating complete ATP problems.

Using MPTP and generating ATP problems requires a quite complex installation and setup (SWI Prolog, Unix, special XSL style sheets, the translated MML in the MPTP format, etc.), so this is a good example of an additional functionality that would be quite hard to provide locally. The MPTP was initially designed for offline production of interesting ATP problems and data, and was not optimized for speed. Several techniques have been used to provide a reasonable real-time experience:

- More advanced (graph-like) data structures have been used to speed up the selection of parts of the MML necessary for generating the ATP problems.

- Larger use has been made of Prolog indexing and the asserted database, for various critical parts of the code.

- The MPTP version of the MML has been factored so that it is possible to work with only the parts of the MML needed for a given article.
These techniques have led to reasonable real-time performance of the MPTP
problem generation, comparable to the performance of Mizar verification and HTMLization. For example, the MPTP processing followed by the generation of all 586 ATP problems for the card 1 article takes 7s on the server.

After the conversion to MPTP format, the ATP problems for an article are generated asynchronously while the user is presented with the HTMLized article.

There is a small danger of the user wanting to solve an ATP problem that has not yet been generated. However, it is easy to check if the translation process is finished, and which ATP problems are already available, by examining the system log.

The MPTP processing has not been parallelized (like the Mizar verification and HTMLization). However, there are no serious obstacles to that. Another speed-up option would be to ask MPTP to generate only a subset of the ATP problems (this is actually how the parallelization is going to work), selected in some reasonable way by the formalizer in the user interface. It is also possible to keep the MPTP system loaded and listening once it has generated a subset of problems, and to have it generate new ATP problems from the current article on demand.

The HTMLization of an article and the generation of ATP problems are independent processes that could be separated into two separate services. Users might, for instance, be interested only in HTML-like disambiguation of their articles, or only in getting explanations and advice from ATP systems, without looking at the HTML form of the article. With sufficient CPU-cores in the server, none of these two possible use-cases suffers in terms of the response time.