> ... I am very excited to see this sort of "codification" work become a legitimate academic enterprise. ... I am a big fan or the sort of thinking ... that we

> ... I am very excited to see this sort of "codification" work become a legitimate academic enterprise. ... I am a big fan or the sort of thinking ... that we need fewer "write an move on" works (e.g. academic papers), and more long-term living documents (e.g. wikis, but not just). You might find the Metamath databases to be very interesting (full disclosure: I participate). In particular, the "Metamath Proof Explorer" (MPE) database uses conventional classical logic + ZFC and proves all sorts of things. It is constantly updated as a collection, and every change is verified by multiple independently-implemented verifiers: http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html Metamath doesn't embed any particular logic or other axioms, so you can choose the axioms you wish. There are other Metamath databases, as shown here at http://us.metamath.org/index.html http://us.metamath.org/index.html , such as the Intuitionistic Logic Explorer (it uses intuitionistic logic instead of classical logic) and the New Foundations Explorer (it constructs mathematics from scratch starting from Quine's NF set theory axioms). Most people have decided to not follow Russell's Typed Set Theory, as his hierarchy of types seems complex to many. If you want to use a more Russell-type system, I think Quine's NF set theory is an elegant simplification of it. You can see more of its Metamath representation here: http://us.metamath.org/nfeuni/mmnf.html http://us.metamath.org/nfeuni/mmnf.html