miz3f
HOL Light theorem prover
Install
- All systems
-
curl cmd.cat/miz3f.sh
- Debian
-
apt-get install hol-light - Ubuntu
-
apt-get install hol-light - Windows (WSL2)
-
sudo apt-get updatesudo apt-get install hol-light - Raspbian
-
apt-get install hol-light - Dockerfile
- dockerfile.run/miz3f
hol-light
HOL Light theorem prover
HOL Light is an interactive theorem prover for Higher-Order Logic with a very simple logical core running in an OCaml toplevel. HOL Light is famous for the verification of floating-point arithmetic as well as for the Flyspeck project, which aims at the formalization of Tom Hales' proof of the Kepler conjecture.