Math Library

Selections from the PRL Math Library

This is a library of fully formalized definitions and proofs. Some of the material has been enhanced by the addition of informal explanations referring to it.

How to browse the library...

There is also a experimental automatic web projection project for the FDL content

The Library

NuprlPrim Standard NumThy1 Lists IrrRoot

Automata ChainRepl EventSys Graphs Hyb.Prots.

Eduprl FTA IterBinops Russells Hanoi

PropCaldwell HOLlib MarkB Amanda2 Zeno

SIPL Turing Bar

Here are some listings of theories developed by Paul Jackson (taken from his full listing):

Algebra Perms1 Perms2 FinMsets Factor

Here is some non-mathematical material.