4 ms·

The Fundamental Theorem of Algebra in ACL2

67 points by luu 5y ago

shoo 5y ago
> We have shown a proof in ACL2(r) of the Fundamental Theorem of Algebra.[...] The proof follows the 1746 proof of d’Alembert, which was maligned by Gauss on the grounds that it was not sufficiently rigorous. Gauss was right, in that it took another hundred years for the notion of continuity to be sufficiently rigorous to prove the Extreme Value Theorem, on which the proof depends I am guessing the Fundamental Theorem of Algebra is a fairly well established and uncontroversial result after 275 years! Can anyone with familiarity of the field explain what the significance of proving this with ACL2(r) is?
- woojoo666 5y ago
  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.
- mhh__ 5y ago
  (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.
  - shoo 5y ago
    i agree that the task of actually searching for a valid proof or counterexample of some hypthosesis (rather than verifying a given purported proof is correct or not with respect to some known axioms/theorems etc) relies on an awfully large amount of intuition & knowledge of standard heuristic "tricks" that might be applied to guide the search. i only took pure math to undergrad level, but sitting in lectures and having a particular proof explained was often fairly frustrating ("why on earth would we think of applying that particular trick there?" "where on earth did that idea come from?") from the perspective of thinking how you (or a machine) might go about methodically discovering a proof for yourself.
GolDDranks 5y ago
I find semi-automaticed theorem proving a very interesting field, because I'm fascinated by axiomatic systems and the fundamentals of logic and maths, but I don't have any experience of using them, yet. What kind of axiomatic basis is being used in ACL2 and similar systems? Is the basics just modus ponens and the axioms are provided as a library? Or do the different systems have significant differences with how and what they can prove? Do the systems allow explorations in reverse maths, trying to derive stuff with as little axioms as possible?
- siraben 5y ago
  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/ https://softwarefoundations.cis.upenn.edu/ [1] (Agda) https://plfa.github.io/ https://plfa.github.io/ [2] (Isabelle) http://concrete-semantics.org/ http://concrete-semantics.org/ [3] (Lean) https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... [4] https://github.com/coq/coq/wiki/The-Logic-of-Coq https://github.com/coq/coq/wiki/The-Logic-of-Coq
- plafl 5y ago
dash2 5y ago
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?
- Y_Y 5y ago
  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.
- siraben 5y ago
  > 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 https://github.com/siraben/math-3100/blob/master/analysis.v [1] https://github.com/coq-community/corn https://github.com/coq-community/corn [2] https://coq.discourse.group/t/interval-4-2-now-with-plotting/1248 https://coq.discourse.group/t/interval-4-2-now-with-plotting... [3] https://hal.inria.fr/hal-00860648v1/document https://hal.inria.fr/hal-00860648v1/document [4] http://ix.io/3rxD http://ix.io/3rxD [5] https://www.math24.net/increasing-decreasing-functions#h-properties-of-monotonic-functions https://www.math24.net/increasing-decreasing-functions#h-pro...
ur-whale 5y ago
For those - like me - who don't know what ACL2 is: https://en.wikipedia.org/wiki/ACL2 https://en.wikipedia.org/wiki/ACL2 It is a environment for formal logic and theorem proving.
ur-whale 5y ago
This paper, from the article's citations is quite nice: https://sci-hub.se/https://doi.org/10.1007/s00283-015-9572-7 https://sci-hub.se/https://doi.org/10.1007/s00283-015-9572-7

67 points by luu 5y ago

shoo 5y ago

> We have shown a proof in ACL2(r) of the Fundamental Theorem of Algebra.[...] The proof follows the 1746 proof of d’Alembert, which was maligned by Gauss on the grounds that it was not sufficiently rigorous. Gauss was right, in that it took another hundred years for the notion of continuity to be sufficiently rigorous to prove the Extreme Value Theorem, on which the proof depends I am guessing the Fundamental Theorem of Algebra is a fairly well established and uncontroversial result after 275 years! Can anyone with familiarity of the field explain what the significance of proving this with ACL2(r) is?

woojoo666 5y ago
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.
mhh__ 5y ago
(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.
- shoo 5y ago
  i agree that the task of actually searching for a valid proof or counterexample of some hypthosesis (rather than verifying a given purported proof is correct or not with respect to some known axioms/theorems etc) relies on an awfully large amount of intuition & knowledge of standard heuristic "tricks" that might be applied to guide the search. i only took pure math to undergrad level, but sitting in lectures and having a particular proof explained was often fairly frustrating ("why on earth would we think of applying that particular trick there?" "where on earth did that idea come from?") from the perspective of thinking how you (or a machine) might go about methodically discovering a proof for yourself.

GolDDranks 5y ago

I find semi-automaticed theorem proving a very interesting field, because I'm fascinated by axiomatic systems and the fundamentals of logic and maths, but I don't have any experience of using them, yet. What kind of axiomatic basis is being used in ACL2 and similar systems? Is the basics just modus ponens and the axioms are provided as a library? Or do the different systems have significant differences with how and what they can prove? Do the systems allow explorations in reverse maths, trying to derive stuff with as little axioms as possible?

siraben 5y ago
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/ https://softwarefoundations.cis.upenn.edu/ [1] (Agda) https://plfa.github.io/ https://plfa.github.io/ [2] (Isabelle) http://concrete-semantics.org/ http://concrete-semantics.org/ [3] (Lean) https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... [4] https://github.com/coq/coq/wiki/The-Logic-of-Coq https://github.com/coq/coq/wiki/The-Logic-of-Coq
plafl 5y ago

dash2 5y ago

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?

Y_Y 5y ago
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.
siraben 5y ago
> 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 https://github.com/siraben/math-3100/blob/master/analysis.v [1] https://github.com/coq-community/corn https://github.com/coq-community/corn [2] https://coq.discourse.group/t/interval-4-2-now-with-plotting/1248 https://coq.discourse.group/t/interval-4-2-now-with-plotting... [3] https://hal.inria.fr/hal-00860648v1/document https://hal.inria.fr/hal-00860648v1/document [4] http://ix.io/3rxD http://ix.io/3rxD [5] https://www.math24.net/increasing-decreasing-functions#h-properties-of-monotonic-functions https://www.math24.net/increasing-decreasing-functions#h-pro...

ur-whale 5y ago

For those - like me - who don't know what ACL2 is: https://en.wikipedia.org/wiki/ACL2 https://en.wikipedia.org/wiki/ACL2 It is a environment for formal logic and theorem proving.

ur-whale 5y ago

This paper, from the article's citations is quite nice: https://sci-hub.se/https://doi.org/10.1007/s00283-015-9572-7 https://sci-hub.se/https://doi.org/10.1007/s00283-015-9572-7