Matita Documentation
User Manual
The Matita User Manual is accessible from Matita itself via the GNOME Help System, just hit <F1> while running Matita and it will be shown to you.
Alternatively you can browse it in XHTML format:
The source code of the user manual (in DocBook format) is available from our repository, in the matita/help/C/ folder.
Tutorials
A not so short tutorial by A.Asperti, discussing some basic notions of number theory, for the stable version of Matita.
A tutorial by E.Tassi based on the formalization of the paper "Between formal topology and game theory: an explicit solution for the conditions for an inductive generation of formal topologies" by S.Berardi and S.Valentini. The tutorial describes the ng version of Matita (not officially released yet, cohexisting with the stable system in version 0.5.8). If some characters are not displayed correctly (i.e. you are not using firefox) you may try the pdf version.
Exercises
Some commented exercises given at the types summer school 2007 by C.Sacerdoti and E.Tassi.