  This article describes a prototype implementation of a web interface for the
Matita proof assistant. The interface supports all basic functionalities of the
local Gtk interface, but takes advantage of the markup to enrich the document
with several kinds of annotations or active elements. Annotations may have both
a presentational/hypertextual nature, aimed to improve the quality of the proof
script as a human readable document, or a more semantic nature, aimed to help
the system in its processing of the script. The latter kind comprises
information automatically generated by the proof assistant during previous
compilations, and stored to improve the performance of re-executing expensive
operations like disambiguation or automation.
