Math Gate

Contact Person
Chad E Brown

Automated Reasoning in Higher Order Logic

Javascript Interactive Higher-Order Theorem Prover

Welcome to Math Gate

The purpose of the Math Gate site is to provide a link between formal (computer checkable) and informal (human readable) mathematics. Currently the main content of the site is an online book (DeTSeT) in which the foundations of mathematics are developed starting from some axioms of set theory. In the future I would like the site to evolve into a formal blog.

Links

The proof checker simptcheck is here, along with checkable formal versions of the DeTSeT items.
I formulated conditions related to consistency of Quine's NF in Simptcheck notation. You can use Simptcheck to verify a solution (which would prove Quine's NF consistent) or to verify a proof that my approach to constructing a model of NF cannot work.
Some exercises using Basil Smith's Elementary Theory of Relations in Jitpro and LEO-II.
Scunak is an interactive theorem prover for set theory in a dependent type theory. It is written in Common Lisp.
Simptcheck is a simple checker for proof terms written in OCaml.