Top 15 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: Why Mathematical Proof Is a Social Compact | | 2023-08-31

    To be ruthlessly, uselessly pedantic - after all, we're mathematicians - there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;)

    But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps more somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory.

    For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely.

    But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel.

    But we've definitely gotten it right this time...


  • FStar

    A Proof-oriented Programming Language

    Project mention: If You've Got Enough Money, It's All 'Lawful' | /r/WorkReform | 2023-05-13

    Don't get me wrong, there are times when Microsoft got it right the first time that was technically far superior to their competitors. Windows IOCP was theoretically capable of doing C10K as far back in 1994-95 when there wasn't any hardware support yet and UNIX world was bickering over how to do asynchronous I/O. Years later POSIX came up with select which was a shoddy little shit in comparison. Linux caved in finally only as recently as 2019 and implemented io_uring. Microsoft research has contributed some very interesting things to computer science like Z3 SAT solver and in collaboration with INRIA made languages like F* and Low* for formal specification and verification. But all this dwarfs in comparison to all the harm they did.

  • SonarQube

    Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.

  • mathlib

    Lean mathematical components library

    Project mention: Towards a new SymPy: part 2 – Polynomials | | 2023-09-08

    It's been on my mind lately as well. I was trying out `symbolics.jl` (a CAS written in Julia), and it turned out that it didn't support symbolic integration beyond simple linear functions or polynomials (at least back then, things have changed now it seems). Implementing a generic algorithm for finding integrals is hard, but I was expecting more from that CAS since this seems to be implemented in most other CASs. The thing is that every single CAS that covers general maths knowledge will have to implement the same algorithm, while it's hard to do it even once!

    I feel like at least a large part of the functionality of a general purpose CAS can be written down once, and every CAS out there could benefit from it, similar to what the Language Server Protocol did for programming tools. They also had to rewrite the same tool for some language multiple times because there are lots of editors out there, and the LSP cut the time investment down a lot. They did have to invest a large amount of time to get LSP up and running, and it'll have to be maintained, but I think it's orders of magnitudes more efficient than having every tool developed and maintained for every single (programming language, editor) pair out there.

    Main problem is like you said how to write down mathematical knowledge in a way that all CASs can understand it. I've been learning about Mathlib lately [0], which seems like a great starting point for this. It is as far as I know one of the first machine readable libraries of mathematical knowledge; it has a large community which has been pushing it continuously forward for years into research-level mathematics and covering the entire undergraduate maths curriculum and it's still accelerating. If some kind of protocol can be designed to read from libraries like this and turn it into CAS code, that would be a major step towards making the CAS ecosystem more sustainable I think.

    It's not exactly what you were talking about, as in, this would allow multiple CASs to co-exist and benefit from each other, but I think that's better than having one massive CAS that has a monopoly. No software is perfect, but having a diverse set of choices that are open source would be more than enough to satisfy everyone.

    (I have posted about this before on the Lean Zulip forum, it's open to everyone to read without an account [1])


  • cakeml

    CakeML: A Verified Implementation of ML

    Project mention: The future of Clang-based tooling | | 2023-07-29

    > A single IR with multiple passes is a good way to build a compiler, which is using, is largely claiming the opposite. Most passes more naturally are not "a -> a", but "a -> b". data structures and data structures work hand in hand, it is very nice to produce "evidence" for what is done in the output data structure.

    This is why, which "can't cheat" with partial functions, has so many IRs!

    Using just a single IR was historically done for cost-control, the idea being that having many IRs was a disaster in repetitive boilerplate. MLIR seeks to solve that exact problem!

  • CoqGym

    A Learning Environment for Theorem Proving with the Coq proof assistant

    Project mention: Discussion Thread | /r/neoliberal | 2023-03-15

    This has been an active area of research for a few years. See for example It's still immature as a field, and most results are essentially "we got basic stuff down but it hasn't gotten powerful enough to prove anything truly challenging" but it definitely exists and is being developed.

  • 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.

  • ProvingGround

    Proving Ground: Tools for Automated Mathematics

  • Mergify

    Updating dependencies is time-consuming.. Solutions like Dependabot or Renovate update but don't merge dependencies. You need to do it manually while it could be fully automated! Add a Merge Queue to your workflow and stop caring about PR management & merging. Try Mergify for free.

  • pyprover

    Resolution theorem proving for predicate logic in pure Python.

    Project mention: First order logic theorem prover in pure Python | | 2023-08-31
  • rusty-razor

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

    Project mention: What is good resource to learn how to convert FOL into CNF? | /r/logic | 2023-02-26

    I’ve implemented these sorts of conversion in Rust (to CNF, DNF, SNF (Skolem normal form), etc.) If you are familiar with the language, feel free to check it out here (under razor-fol): (there’s extensive documentation that you can check out after running cargo doc. Also I should point out that later I realized that having two forms of CNF (or DNF), one before Skolemization and one after (dropping existentials) comes handy for conversion to various forms, especially what I’m interested in Geometric Logic. That work isn’t completely ready to land to the main branch but it’s pretty complete and you can check it out in the fix-transform branch.

  • ewd998

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

    Project mention: How to specify "After P is true, Q is always true"? | /r/tlaplus | 2023-03-30

    You might find useful, where you can explicitly define a set of behaviors (see `seq`), and have TLC check your temporal properties (see `Prop`).

  • 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)

    Project mention: What would you rewrite in Rust? | /r/rust | 2023-02-11

    This may interest you:

  • InfluxDB

    Collect and Analyze Billions of Data Points in Real Time. Manage all types of time series data in a single, purpose-built database. Run at any scale in any environment in the cloud, on-premises, or at the edge.

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). The latest post mention was on 2023-09-08.

theorem-proving related posts


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

Project Stars
1 coq 4,367
2 FStar 2,468
3 mathlib 1,604
4 cakeml 854
5 CoqGym 340
6 awesome-rust-formalized-reasoning 227
7 ProvingGround 200
8 pyprover 77
9 rusty-razor 55
10 ewd998 42
11 trepplein 26
12 zsyntax 10
13 tptp 6
14 supervisionary 3
15 supervisionary 0
Collect and Analyze Billions of Data Points in Real Time
Manage all types of time series data in a single, purpose-built database. Run at any scale in any environment in the cloud, on-premises, or at the edge.