Megalodon is an interactive theorem prover/proof checker based on higher-order Tarski-Grothendieck set theory. It is the successor system to Egal [1].

Megalodon is like

• AUTOMATH (since the focus is on constructing documents consisting of definitions and theorems, with theorems proven by simple Curry-Howard style proof terms)
• Coq (since the basic tactics for constructing proofs mirror those in Coq)
• Mizar and MetaMath (since the foundation is a form of Tarski-Grothendieck, but in higher-order order)
• and Isabelle/HOL and other HOL systems (since the underlying framework is simply typed).

Here is an html presentation of a formal development in Megalodon including proofs of 12 of the 100 theorems often used as a benchmark for interactive provers.

Megalodon is written in OCaml, which should be the only dependency you need to compile it.

A recent release of Megalodon is 1.13.

Starting with Version 1.13, subproofs can be justified by the hammer tactic and calls to ATPs. See examples/hammer/README for more information.

Other versions of Megalodon can be found here and here.

[1] Brown, Chad E. and Pąk, Karol. A tale of two set theories. CICM 2019. pp 44-60