Top 16 theorem-proving Open-Source Projects

• coq

  88 4,875 10.0 OCaml

  Coq is a formal proof management system. 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.

  

  Project mention: Coq will be renamed into 'The Rocq Prover' | news.ycombinator.com | 2024-08-07

• CodeRabbit

  coderabbit.ai featured

  CodeRabbit: AI Code Reviews for Developers. Revolutionize your code reviews with AI. CodeRabbit offers PR summaries, code walkthroughs, 1-click suggestions, and AST-based analysis. Boost productivity and code quality across all major languages with each PR.

  

• FStar

  44 2,701 9.9 F*

  A Proof-oriented Programming Language

  

  Project mention: F* – A Proof-Oriented Programming Language | news.ycombinator.com | 2024-05-16

• LeanCopilot

  8 1,009 8.9 C++

  LLMs as Copilots for Theorem Proving in Lean

  

  Project mention: LeanDojo: Theorem Proving in Lean Using LLMs | news.ycombinator.com | 2024-07-28

• cakeml

  15 972 9.9 Standard ML

  CakeML: A Verified Implementation of ML

  

  Project mention: CakeML: A formally verified implementation of ML | news.ycombinator.com | 2024-05-14

• CoqGym

  2 382 3.6 Coq

  A Learning Environment for Theorem Proving with the Coq proof assistant

  

• awesome-rust-formalized-reasoning

  3 301 7.7

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

• ProvingGround

  1 203 2.6 Jupyter Notebook

  Proving Ground: Tools for Automated Mathematics

• SaaSHub

  www.saashub.com featured

  SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

  

• LeanDojoChatGPT

  2 113 5.3 Python

  ChatGPT plugin for theorem proving in Lean

  

• pyprover

  1 91 3.6 Python

  Resolution theorem proving for predicate logic in pure Python.

• rusty-razor

  1 55 10.0 Rust

  Razor is a tool for constructing finite models for first-order theories

• ewd998

  2 50 0.0 TLA

  Distributed termination detection on a ring, due to Shmuel Safra:

  

• trepplein

  2 26 0.0 Scala

  Lean type-checker written in Scala.

• zsyntax

  0 11 6.6 Haskell

  Automated theorem prover for a linear logic-based calculus for molecular biology.

• tptp

  0 7 0.0 Haskell

  Parser and pretty printer for the TPTP language

• supervisionary

  1 3 3.2 Rust

  The Supervisionary proof-checking kernel for higher-order logic

  

• supervisionary

  1 0 1.6 Rust

  Supervisionary: a proof-checking system for HOL (by DominicPM)

• SaaSHub

  www.saashub.com featured

  SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

  

theorem-proving related posts

• Coq will be renamed into 'The Rocq Prover'

  1 project | news.ycombinator.com | 7 Aug 2024

• LeanDojo: Theorem Proving in Lean Using Language Models

  1 project | news.ycombinator.com | 26 Jul 2024

• AI solves IMO problems at silver medal level

  2 projects | news.ycombinator.com | 26 Jul 2024

• CakeML: A formally verified implementation of ML

  1 project | news.ycombinator.com | 14 May 2024

• Change of Name: Coq –> The Rocq Prover

  3 projects | news.ycombinator.com | 26 Dec 2023

• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

  1 project | /r/math | 11 Dec 2023

• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

  1 project | /r/math | 11 Dec 2023
• A note from our sponsor - CodeRabbit
  coderabbit.ai | 10 Dec 2024

  Revolutionize your code reviews with AI. CodeRabbit offers PR summaries, code walkthroughs, 1-click suggestions, and AST-based analysis. Boost productivity and code quality across all major languages with each PR. Learn more →

Index

Sponsored

CodeRabbit: AI Code Reviews for Developers

Revolutionize your code reviews with AI. CodeRabbit offers PR summaries, code walkthroughs, 1-click suggestions, and AST-based analysis. Boost productivity and code quality across all major languages with each PR.

coderabbit.ai