A library of formalized mathematics for Isabelle/ZF theorem proving environment

About this site

This site is an experimental HTML rendering of fragments of the IsarMathLib project. IsarMathLib is a library of mathematical proofs formally verified by the Isabelle theorem proving environment. The formalization is based on the Zermelo-Fraenkel set theory. The Introduction provides more information about IsarMathLib.

The software for exporting Isabelle's Isar language to HTML markup is at an early beta stage, so some proofs may be rendered incorrectly. In case of doubts, compare with the Isabelle generated IsarMathLib proof document.

Mathematical notation on this site is rendered by MathJax. MathJax is an implementation of TeX layout algorithms in JavaScript. After loading a page you may see the LaTeX markup instead of mathematical notation for a second or two before MathJax script renders the math symbols.