corn
UniMath
| corn | UniMath | |
|---|---|---|
| 1 | 2 | |
| 108 | 912 | |
| 0.9% | 0.7% | |
| 6.8 | 9.5 | |
| 9 days ago | 1 day ago | |
| Coq | Coq | |
| GNU General Public License v3.0 only | GNU General Public License v3.0 or later |
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.
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...
UniMath
-
Will Computers Redefine the Roots of Math?
For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:
UniMath (https://github.com/UniMath/UniMath, mentioned in the article)
Coq-HoTT (https://github.com/HoTT/Coq-HoTT)
agda-unimath (https://unimath.github.io/agda-unimath/)
cubical agda (https://github.com/agda/cubical)
All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).
-
Are There People Doing Formal Math In Berlin?
I just wonder if there are any irl meetups of people involved with formalizing mathematics, I thought that it would be a cool hobby to pick up (with some background in math and programming) but the existing libraries, like MathLib, TypeTopology or UniMath look a bit intimidating...
What are some alternatives?
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.
math-comp - Mathematical Components
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.
Coq-HoTT - A Coq library for Homotopy Type Theory
fourcolor - Formal proof of the Four Color Theorem [maintainer=@ybertot]
nqthm - nqthm - the original Boyer-Moore theorem prover, from 1992
TypeTopology - Logical manifestations of topological concepts, and other things, via the univalent point of view.
hs-to-coq - Convert Haskell source code to Coq source code.
rupicola - Gallina to Bedrock2 compilation toolkit