Debian logoDebian Screenshots >


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.

Upload more screenshots

Please help extend the collection of screenshots. Just make a screenshot and upload it here. You don't need to register or anything.



1858 other people were interested in this package here. The newest known version of this software is 20190729-4+b2 (Information last updated 1 day ago.)