Matita[1] is an experimental proof assistant under development at the Computer Science Department of the University of Bologna.

The word "matita" means "pencil" in Italian (a simple and widespread editing tool).

It is a reasonably small and simple application,[2] whose architectural and software complexity is meant to be mastered by students, providing a tool particularly suited for testing innovative ideas and solutions.

Matita adopts a tactic-based editing mode; (XML-encoded) proof objects are produced for storage and exchange.

The power of the type inference system (refiner) is further augmented by a mechanism of hints[5] that helps in synthesizing unifiers in particular situations specified by the user.