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 it contains a formalization of elementary topology and the game of Go/Igo/Weiqi/Baduk (both are 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 license header is even more concise than the license of Expat (so called “MIT license”). The reader is encouraged to use this license for his own projects 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