theorem-proving

Star

Here are 260 public repositories matching this topic...

Language:All

Filter by language

All260 Python36 Lean33 Rocq Prover25 OCaml15 Agda12 Isabelle11 Haskell10 Rust10 Scala10 Standard ML10

Sort:Most stars

Sort options

Most stars Fewest stars Most forks Fewest forks Recently updated Least recently updated

rocq-prover /rocq

Star5.2k

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

dependent-types coq theorem-proving proof-assistant

UpdatedJul 17, 2025
OCaml

FStarLang /FStar

Star2.9k

A Proof-oriented Programming Language

programming-language dependent-types ocaml theorem-proving verification f-sharp proof-assistant smt c-language fstar

UpdatedJul 18, 2025
F*

leanprover /lean3

Star2.2k

Lean Theorem Prover

programming-language dependent-types theorem-proving verification type-theory lean

UpdatedOct 14, 2023
C++

leanprover-community /mathlib3

Star1.7k

Lean 3's obsolete mathematical components library: please use mathlib4

theorem-proving lean formal-methods formal-mathematics proof-automation formal-proofs

UpdatedJun 28, 2024
Lean

lean-dojo /LeanCopilot

Star1.1k

LLMs as Copilots for Theorem Proving in Lean

machine-learning theorem-proving lean formal-mathematics lean4 llm-inference

UpdatedJul 13, 2025
C++

CakeML /cakeml

Star1.1k

CakeML: A Verified Implementation of ML

programming-language compiler formal-semantics theorem-proving sml formal-verification hol

UpdatedJul 18, 2025
Standard ML

lean-dojo /LeanDojo

Star678

Tool for data extraction and interacting with Lean programmatically.

machine-learning theorem-proving lean lean4

UpdatedJun 13, 2025
Python

HOL-Theorem-Prover /HOL

Star675

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.

lambda-calculus theorem-proving higher-order-logic

UpdatedJul 18, 2025
Standard ML

idris-hackers /software-foundations

Star454

Software Foundations in Idris

computer-science book theorem-proving idris

UpdatedMay 15, 2019
Idris

princeton-vl /CoqGym

Star405

A Learning Environment for Theorem Proving with the Coq proof assistant

machine-learning theorem-proving icml-2019

UpdatedJun 30, 2023
Coq

dselsam /certigrad

Star395

Bug-free machine learning on stochastic computation graphs

machine-learning theorem-proving verification lean

UpdatedMar 3, 2019
Lean

acl2 /acl2

Star395

ACL2 System and Books as Maintained by the Community

common-lisp logic theorem-proving first-order-logic formal-methods formal-verification theorem-prover rewriting acl2

UpdatedJul 18, 2025
Common Lisp

johnyf /tool_lists

Star378

Links to tools by subject

tools static-analysis theorem-proving verification proof-assistant smtlib synthesis satisfiability-solver binary-decision-diagrams model-checking satisfiability-modulo-theories formal-methods theorem-prover

UpdatedMar 19, 2024

newca12 /awesome-rust-formalized-reasoning

Star346

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

rust dependent-types logic theorem-proving formal-verification prover automated-theorem-provers reasoning theorem-prover constructive-mathematics proof-assistants