SourceForge.net

In the tradition of Hilbert`s program we create a formal correct (checkable by a proof verifier) but readable (like an ordinary LaTeX textbook) mathematical knowledge base which is freely accessible within the internet. We start with logic and set theory