theorem-proving

Open-source projects categorized as theorem-proving
Edit details
Language: + Rust + Haskell + OCaml + F* + Lean + Standard ML + C++ + Coq + Jupyter Notebook + Python + TLA + Scala
Topics: theorem-prover Dependent Types Lean programming-language proof-assistant
Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
Sponsored

Top 16 theorem-proving Open-Source Projects

  • coq

    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: Change of Name: Coq –> The Rocq Prover | news.ycombinator.com | 2023-12-26

    The page summarizing the considered new names and their pros/cons is interesting: https://github.com/coq/coq/wiki/Alternative-names

    Naming is hard...

  • FStar

    A Proof-oriented Programming Language

    • Project mention: Lean4 helped Terence Tao discover a small bug in his recent paper | news.ycombinator.com | 2023-10-27

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo

  • mathlib

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

    • Project mention: An Easy-Sounding Problem Yields Numbers Too Big for Our Universe | news.ycombinator.com | 2023-12-04

  • cakeml

    CakeML: A Verified Implementation of ML

    • Project mention: The Deep Link Equating Math Proofs and Computer Programs | news.ycombinator.com | 2023-10-11

    If I understand what you are asking about correctly, then I do think you are mistaken.

    As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done.

    This ranges from things like CakeML (https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages.

    Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.

  • LeanCopilot

    LLMs as Copilots for Theorem Proving in Lean

    • Project mention: New Foundations is consistent – a difficult mathematical proof proved using Lean | news.ycombinator.com | 2024-04-23

    Then it's time to update your LLM reading!

    https://leandojo.org/

  • CoqGym

    A Learning Environment for Theorem Proving with the Coq proof assistant

    • Project mention: Lean4 helped Terence Tao discover a small bug in his recent paper | news.ycombinator.com | 2023-10-27

  • awesome-rust-formalized-reasoning

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

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

    WorkOS logo

  • ProvingGround

    Proving Ground: Tools for Automated Mathematics

  • pyprover

    Resolution theorem proving for predicate logic in pure Python.

    • Project mention: First order logic theorem prover in pure Python | news.ycombinator.com | 2023-08-31

  • rusty-razor

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

  • ewd998

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

  • trepplein

    Lean type-checker written in Scala.

  • zsyntax

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

  • tptp

    Parser and pretty printer for the TPTP language

  • supervisionary

    The Supervisionary proof-checking kernel for higher-order logic

  • supervisionary

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

  • SaaSHub

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

    SaaSHub logo
NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020).

theorem-proving related posts

Index

What are some of the best open-source theorem-proving projects? This list will help you:

Project Stars
1 coq 4,602
2 FStar 2,562
3 mathlib 1,625
4 cakeml 912
5 LeanCopilot 672
6 CoqGym 370
7 awesome-rust-formalized-reasoning 263
8 ProvingGround 202
9 pyprover 87
10 rusty-razor 55
11 ewd998 46
12 trepplein 26
13 zsyntax 11
14 tptp 6
15 supervisionary 3
16 supervisionary 0

Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com