Matita is a new, document-centric, tactic-based interactive theorem prover. This paper focuses on some of the distinctive
features of the user interaction with Matita, characterized mostly by the organization of the library as a searchable knowledge
base, the emphasis on a high-quality notational rendering, and the complex interplay between syntax, presentation, and semantics.
Keywords Proof assistant - Interactive theorem proving - Digital libraries - XML - Mathematical knowledge management - Authoring
“We are nearly bug-free” – CSC, Oct. 2005.