+\section{The logical library}
+Matita is Coq compatible, in the sense that every theorem of Coq
+can be read, checked and referenced in further developments.
+However, in order to test the actual usability of the system, a
+new library of results has been started from scratch. In this case,
+of course, the user may also dispose of the source script files,
+while in the case of Coq he may only rely on XML files of
+Coq objects.
+The current library just comprises about one thousand theorems in
+elementary aspects of arithmetics. The most complex result proved
+so far in Matita (that however, at our knoweledge, has never been proved
+before in any other system) is the multiplicative property for Eulers'
+totient function $\phi$.
+The library is organized in five main directories: $logic$ (connectives,
+quantifiers, equality, $\dots$), $datatypes$ (basic datatypes and type
+constructors), $nat$ (natural numbers), $Z$ (integers), $Q$ (rationals).
+The most complex development is $nat$, organized in 25 scripts, listed
+in Figure\ref{scripts}
+\begin{figure}[htb]
+$\begin{array}{lll}
+nat.ma & plus.ma & times.ma \\
+minus.ma & exp.ma & compare.ma \\
+orders.ma & le\_arith.ma & lt\_arith.ma \\
+factorial.ma & sigma\_and\_pi.ma & minimization.ma \\
+div\_and\_mod.ma & gcd.ma & congruence.ma \\
+primes.ma & nth\_prime.ma & ord.ma\\
+count.ma & relevant\_equations.ma & permutation.ma \\
+factorization.ma & chinese\_reminder.ma & fermat\_little\_th.ma \\
+totient.ma& & \\
+\end{array}$
+\caption{\label{scripts}Matita scripts on natural numbers}
+\end{figure}
+
+We do not plan to maintain the library in a centralized way,
+as most of the systems do. On the contary we are currently
+developing wiki-technologies to support a collaborative
+development of the library, encouraging people to expand,
+modify and elaborate previous contributions.
+
+