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. Logic and set theory started.
Open source project that offer summary and download services on this page is a project that carry out their development work on other open source development sites. Their work is linked to this page via a feature called OFI, and their work is not carried out here on OSDN site.
