Hacker News Reader

Comment by dash2 | Hacker News Reader

What I want to know is, when are automated provers gonna be useful for thickies like me?

That is, I'm an economist and I regularly want to prove stuff that would be far below the level of a real mathematician. Simple problems in R or R^N with continuous functions and maybe the output will be "such and such an optimal solution is increasing in some parameter". Right now there's mathematica, which can be useful but won't really do stuff on its own - it'll rearrange an equation but I can't ask it "prove this is increasing". Or there are these high level systems for proving deep theorems. Is anyone trying to fill the gap?

View on HN

Mathematica's rearrangement is really the same thing (except that usually you don't see the intermediate steps or what inference rules justify them). I think the particular example you mention isn't far away from being available through whatever natural language thing they have. There are lots of existing theorems about e.g. increasing sequences that rely on showing a particular quantity is positive. You can pretty much do that right now, by say, using the ratio test, or some other De Morgan-type test, and then asking your CAS to express it as as a perfect square, or symbolically find its global minimum and asymptotes. Right now I think your best bet is still to employ a student intern though.

Formalizing anything in a proof assistant such as Coq multiplies the amount of work required by orders of magnitude. Proving something on a computer almost universally requires way more ingenuity than proving it on paper.

> Is anyone trying to fill the gap?

I don't think that the state of things is likely to improve because automatic theorem proving is equivalent to the halting problem.

What you're describing is work that is best suited for computer algebra software.

I would say that the vast majority of "real mathematicians" could not use such a proof system either - this is one of the major obstacles stopping the adoption of proof systems or proof assistants in the mathematical community. I think that even at the moment, what proof systems can prove is far far ahead of what regular users can easily express in those proof systems, and there really needs to be some programming language / human-computer-interaction work or research to bridge the gap there.

> What I want to know is, when are automated provers gonna be useful for thickies like me?

Note that automated theorem provers is not the same as proof assistant. With ATPs you delegate most of the work to some proof search, whereas with proof assistants the human drives most of the work (which is more manual but lets you tackle much more complex and undecidable domains).

> Right now there's mathematica, which can be useful but won't really do stuff on its own - it'll rearrange an equation but I can't ask it "prove this is increasing".

The problem with Mathematica (and others) it is both unverified and proprietary, so if your work relies on it you are depending on a huge trusted code base not having mistakes (extremely unlikely).

I recently took an undergraduate course on real analysis, and was able to formalize quite a bit (within reason) from the class in Coq[0]. In fact, it even aided my reasoning, for instance I wasn't ensure the following inequality was true, but Coq made quick work of it.

  Lemma test2 :
    forall (x y z d : R),
      Rabs (z - y) < d ->
      Rabs (x - z) < Rabs (z - (y - d)) ->
      Rabs (x - z) < Rabs (z - (y + d)) ->
      Rabs (x - y) < d.
  Proof. intros; split_Rabs; lra. Qed.

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

Reply on news.ycombinator.com