We plea the need for a rapid - content based - integration of tools for the mechanization of mathematics and the automation of formal reasoning with the World Wide Web. The main point is to have free access to the information "in the Web way", that is with few basic rules and no central autorithy. The final aim is to build a minimal technological infrastructure (based on XML technology) for the creation and maintenance of a virtual, distributed hypertextual library of formal mathematical knowledge.