The Fundamental Theorem of Algebra in ACL2

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.

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

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.

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.

The kernel of a proof assistant is one of the most important components because it represents the foundation of reasoning in that logical system. There's a lot of introductory literature now, such as [0][1][2][3].

> What kind of axiomatic basis is being used in ACL2 and similar systems?

ACL2 uses first-order logic and term rewriting, but this significantly hinders proof automation (done by ad-hoc searches).

> Or do the different systems have significant differences with how and what they can prove?

Yes. First-order logic can only quantify over individual elements of a set, second-order logic can quantify over sets, and so on. Higher-order logic is the foundation of assistants like Isabele/HOL light, which let you use classical reasoning.

Alternatively (and better from an engineering standpoint) are assistants based on type theory, such as Agda, Coq and Lean. Their kernels are just type checkers, which are relatively small programs, so theorem proving in those systems is literally just functional programming with a fancy type system (though exactly how those proofs are constructed is a UX choice).

> Do the systems allow explorations in reverse maths, trying to derive stuff with as little axioms as possible?

Yes, in Coq you can print out the axioms (on top of the type system) that a result depends on. See [4] for information on Coq's logic and what axioms you can safely add (they are necessary for certain areas of math).

[0] (Coq) https://softwarefoundations.cis.upenn.edu/

[1] (Agda) https://plfa.github.io/

[2] (Isabelle) http://concrete-semantics.org/

[3] (Lean) https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...

[4] https://github.com/coq/coq/wiki/The-Logic-of-Coq

If you want a gentle introduction you may like this book http://the-little-prover.github.io/

Any dependent type theory is "semi-automated" because judgemental equality computes normal forms, there is no reason it should be this way, other than convenience of course.

even if a proof is well established, porting it to a proof language allows other proofs to build upon it, like importing dependencies in traditional software development. And the bigger the library of proofs gets, the more possibilities there are for things like automating proofs using search/AI. But I think on top of that, it just serves as a cool milestone because I've heard some people say porting all of mathemetics will take decades, so seeing fundamental theorems like this make it in marks great progress.

(Computer) Theorem proving shows how much we take human reasoning for granted. The computer has no intuition, so proving just about anything interesting requires real skill.