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 semiinteractive development of machinechecked proofs.

SaaSHub
SaaSHub  Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives


coqlibraryundecidability
A library of mechanised undecidability proofs in the Coq proof assistant.


math3100
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 discussion
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 userfriendly 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/math3100/blob/master/analysis.v
[1] https://github.com/coqcommunity/corn
[2] https://coq.discourse.group/t/interval42nowwithplotting...
[3] https://hal.inria.fr/hal00860648v1/document
[4] http://ix.io/3rxD
[5] https://www.math24.net/increasingdecreasingfunctions#hpro...
Stats
coqcommunity/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.