We present and discuss a few statitiscal data on the mathematical library of the Coq Proof Assistant. The ambitious aim of this research is to promote a new field of research in Mathematical Knowledge Management, namely the mathematical investigation of the practice of mathematics. The modest, practical aim is to test a set of metadata we recently introduced for automatic indexing and retrieving of mathematical statements.