corn VS coq-library-undecidability

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

I want to run guix shell to create an environment with the dependencies required to build coq-library-undecidability.

There are two problems. The first is that there is no central repository. Sure, maybe if you're interested in undecidable results you might go here... But it's an island, and so is every other library. Worse yet, there's little inter mixing or combinable ways to use libraries. Unlike other programming languages, automated proof systems have so far been aimed at the technical aspects of a single person proving something, rather than the shareability of proofs.