awesome-interactive-theorem-prover

KO | EN

gitlite — search

#python #java #python3 #arduino #golang #machine-learning #rust #html #flask #javascript #seismology #nodejs

awesome-interactive-theorem-prover

★ 23 Open GitHub ↗

A curated list of awesome interactive theorem prover frameworks

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# Awesome Interactive Theorem Provers [![Awesome](https://awesome.re/badge.svg)](https://awesome.re)

> A curated list of interactive theorem provers, proof assistants, and formal verification systems.

## Commercial Platform
- [Isabelle](https://isabelle.in.tum.de) - Interactive theorem prover based on higher-order logic, widely used for formal verification and mathematics.
- [Why3](https://why3.org) - Platform for deductive program verification integrating multiple theorem provers and SMT solvers.

## Open-Source Project

- [Agda](https://github.com/agda/agda) ![](https://img.shields.io/github/stars/agda/agda.svg?cacheSeconds=86400) - Dependently typed functional programming language and proof assistant with a focus on constructive mathematics.
- [CakeML](https://github.com/CakeML/cakeml) ![](https://img.shields.io/github/stars/CakeML/cakeml.svg?cacheSeconds=86400) - Verified implementation of a substantial subset of Standard ML, with a compiler proven correct in HOL4.
- [F*](https://github.com/FStarLang/FStar) ![](https://img.shields.io/github/stars/FStarLang/FStar.svg?cacheSeconds=86400) - Verification-oriented programming language developed by Microsoft Research with support for effectful programs and SMT-based automation.
- [HOL4](https://github.com/HOL-Theorem-Prover/HOL) ![](https://img.shields.io/github/stars/HOL-Theorem-Prover/HOL.svg?cacheSeconds=86400) - Interactive theorem prover for higher-order logic (HOL4) with strong support for formalized mathematics, semantics, and verified systems.
- [HOL Light](https://github.com/jrh13/hol-light) ![](https://img.shields.io/github/stars/jrh13/hol-light.svg?cacheSeconds=86400) - Interactive theorem prover for higher-order logic developed by John Harrison, known for lightweight design and foundational formalization work.
- [Lean 4](https://github.com/leanprover/lean4) ![](https://img.shields.io/github/stars/leanprover/lean4.svg?cacheSeconds=86400) - Modern theorem prover and functional programming language with a focus on interactive proofs and dependent types.
- [Mathlib4](https://github.com/leanprover-community/mathlib4) ![](https://img.shields.io/github/stars/leanprover-community/mathlib4.svg?cacheSeconds=86400) - The main mathematical library for Lean 4, covering a wide range of undergraduate and graduate mathematics.
- [Rocq](https://github.com/rocq-prover/rocq) ![](https://img.shields.io/github/stars/rocq-prover/rocq.svg?cacheSeconds=86400) - Interactive proof assistant based on the Calculus of Inductive Constructions, formerly known as Coq.

## Contributing

Contributions are welcome! Please feel free to submit a pull request to add more interactive theorem provers to this awesome list.

awesome-interactive-theorem-prover

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README