 The Metamath Proof Explorer references many text books that can be used in conjunction with Metamath.Thus, people interested in studying mathematics can use Metamath in connection with these books and verify that the proved assertions match the literature.This database develops mathematics from a constructive point of view, starting with the axioms of intuitionistic logic and continuing with axioms of constructive set theory.