Corn Alternatives
Similar projects and alternatives to corn based on common topics and language
-
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.
-
-
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.
-
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
-
math-3100
Discontinued My solutions to MATH 3100 (Introduction to Real Analysis) at Vanderbilt University.
-
-
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
corn reviews and mentions
-
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
[5] https://www.math24.net/increasing-decreasing-functions#h-pro...
Stats
coq-community/corn is an open source project licensed under GNU General Public License v3.0 only which is an OSI approved license.
The primary programming language of corn is Coq.
