The open source project Hilbert II provides a program suite that enables a mathematician to put theorems and proofs into that knowledge base. These proofs are automatically verified by a proof checker. Also texts in "common mathematical language" can be integrated.

The mathematical axioms, definitions and propositions are combined to so called QEDEQ modules. Such a module could be seen as a mathematical textbook which includes formal correct proofs. Because this system is not centrally administrated and references to any location in the internet are possible, a world wide mathematical knowledge base could be build. Any proof of a theorem in this "mathematical web" could be drilled down to the very elementary rules and axioms. Think of an incredible number of mathematical textbooks with hyperlinks and each of its proofs could be verified by Hilbert II. For each theorem the dependency of other theorems, definitions and axioms could be easily derived.