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. Learn more →
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.
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...
-
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.
-
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])
-
> A single IR with multiple passes is a good way to build a compiler
https://mlir.llvm.org/, 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 https://cakeml.org/, 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!
-
This has been an active area of research for a few years. See for example https://arxiv.org/abs/1905.09381. 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.
-
-
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.
-
Project mention: First order logic theorem prover in pure Python | news.ycombinator.com | 2023-08-31
-
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): https://github.com/salmans/rusty-razor/tree/master/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.
-
You might find https://github.com/tlaplus-workshops/ewd998/blob/main/TemporalLogic.tla useful, where you can explicitly define a set of behaviors (see `seq`), and have TLC check your temporal properties (see `Prop`).
-
-
-
-
-
This may interest you: https://github.com/DominicPM/supervisionary
-
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
- Towards a new SymPy: part 2 – Polynomials
- Lean 4.0.0, first official lean4 release
- Why Mathematical Proof Is a Social Compact
- The future of Clang-based tooling
- It's not mathematics that you need to contribute to (2010)
- If given a list of properties/definitions and relationship between them, could a machine come up with (mostly senseless, but) true implications?
- Will Computers Redefine the Roots of Math?
-
A note from our sponsor - SonarQube
www.sonarqube.org | 29 Sep 2023
Index
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.
www.influxdata.com