mainFormalization of mathematics in higher order logic (HOL4 proof assistant) - Summary

Show feedback again
Membership Info
Project Admin:
1 active member

Group identification
Id: #257
System Name: hol-proofs
Name: Formalization of mathematics in higher order logic (HOL4 proof assistant)
Group Type: Software

Search in this Group


Free Software

This is an archive of computer-verified formalization of mathematics in HOL4. Currently the only content is a formalization of elementary topology which is still work in progress. For the the work itself see the Mercurial repository:

This work is licensed under the GNU General Public License version 3 or later, plus an exception to allow redistribution without the license text. The resulting license header is even more concise than the license of Expat (so called “MIT license”). The reader is encouraged to apply this license to his own project instead of a pushover (non-copyleft) license.

Registration Date: Sun 01 Oct 2017 07:41:42 PM EEST
License: GNU General Public License V3 or later
Development Status: 0 - Undefined


Quick Overview

Show feedback again

Back to the top

Powered by Savane 3.1-cleanup+gray