3 ms·

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

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

by shoo 5y ago

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.