Magic tree

The goal of the OpenTheory project is to allow specifications and proofs to be shared between different theorem prover implementations of higher order logic, including HOL Light, HOL4 and ProofPower. It is hoped that OpenTheory packages are adopted by the higher order logic theorem proving community as a common format to build a standard library of formalized mathematics and verified software.

Get started with OpenTheory by downloading the opentheory tool.



Theorem Prover Interfaces

Here are the current theorem prover implementations that can read (R) and/or write (W) theories in OpenTheory format:

Theorem ProverR/WMaintainer
HOL LightR/WJoe Leslie-Hurd
HOL4R/WRamana Kumar
ProofPowerR/WRob Arthan
IsabelleRRamana Kumar and Michael Norrish