Corn Alternatives

corn reviews and mentions

• The Fundamental Theorem of Algebra in ACL2
  3 projects | news.ycombinator.com | 29 Jul 2021

  > 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...