To browse the library, type in the location bar the absolute URI of the theorem, definition or library fragment you are interested in. "cic:/" is the root of the library. Contributions developed in Matita are under "cic:/matita"; all the others are part of the library of Coq.

Following the hyperlinks it is possible to navigate in the Web of mathematical notions. Proof are rendered in pseudo-natural language and mathematical notation is used for formulae. For now, mathematical notation must be included in the current script to be activated, but we plan to remove this limitation.

A proof under development is not yet part of the library. The special URI "about:proof" can be used to browse the proof currently under development, if there is one. The "home" button of the CIC browser sets the location bar to "about:proof".