Fast parallel calculations in pure mathematics, e.g. Gröbner Bases

The HOL Light theorem prover

Interface between Isabelle/HOL and OpenTheory

Convert to/from IEEE-754 HP/SP/DP formats

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

ProofPower is an open source suite of tools for specification and proof in HOL and Z.

pp-contrib is a collection of contributed examples and tools for ProofPower users.

HOL Light with OpenTheory Support

Specialized hardware to open the crypto timelock puzzle