fourcolor
corn
Our great sponsors
| fourcolor | corn | |
|---|---|---|
| 2 | 1 | |
| 150 | 108 | |
| 2.7% | 0.0% | |
| 4.6 | 6.8 | |
| 28 days ago | 8 days ago | |
| Coq | Coq | |
| GNU General Public License v3.0 or later | GNU General Public License v3.0 only |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
fourcolor
-
On the Four Color Problem
Takes around 15 minutes on my machine.
[0] https://github.com/coq-community/fourcolor
[1] https://github.com/NixOS/nixpkgs/blob/master/pkgs/developmen...
- Solution to the four color theorem in haskell
corn
-
The Fundamental Theorem of Algebra in ACL2
> Or there are these high level systems for proving deep theorems. Is anyone trying to fill the gap?
There's ongoing work on computable real numbers for instance the CoRN library[1], so hope is on the horizon, for instance, a recent update to the Coq Interval package adds certified plotting, that is, the library guarantees that if a function passes through a pixel, that pixel is filled[2]. There's also the user-friendly Coquelicot[3] real analysis library up to basic differential equations (e.g. Bessel function).
> It'll rearrange an equation but I can't ask it "prove this is increasing"
For a taste, here's my proof that the cube function is increasing[4]. If I wanted to create a tactic that automatically proves a function is increasing, I would use properties of increasing functions[5] to recursively break it down into trivial subcases.
[0] https://github.com/siraben/math-3100/blob/master/analysis.v
[1] https://github.com/coq-community/corn
[2] https://coq.discourse.group/t/interval-4-2-now-with-plotting...
[3] https://hal.inria.fr/hal-00860648v1/document
[4] http://ix.io/3rxD
[5] https://www.math24.net/increasing-decreasing-functions#h-pro...
What are some alternatives?
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.
CompCert - The CompCert formally-verified C compiler
analysis - Mathematical Components compliant Analysis Library
coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
regexp-Brzozowski - Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]
math-comp - Mathematical Components
nixpkgs - Nix Packages collection & NixOS