3 ms·

I didn't know there was software to verify mathematical proofs. Heck, I didn't even know there was a formal syntax for writing them.

• netrus 13y ago
  A prominent example for proofs by computer algorithms is the 4 color theorem: http://en.wikipedia.org/wiki/Four_color_theorem http://en.wikipedia.org/wiki/Four_color_theorem
  • aardvark179 13y ago
    That's not quite the same thing. The 4 colour theorem was proved by boiling it down to several thousand test cases and using a computer program to test those by colouring them. This paper is about using theorem provers to check axioms for consistency and proofs derived from those.
• dylandrop 13y ago
  See http://en.wikipedia.org/wiki/Automated_theorem_proving#Decidability_of_the_problem http://en.wikipedia.org/wiki/Automated_theorem_proving#Decid... Important to note Gödel's completeness theorem here! You might be even more interested in Prolog, a language which has a close relationship with this stuff: "Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of relations, represented as facts and rules. A computation is initiated by running a query over these relations." (http://en.wikipedia.org/wiki/Prolog http://en.wikipedia.org/wiki/Prolog) This is why everyone should take an AI class.
  • lutusp 13y ago
    > Important to note Gödel's completeness [sic] theorem [sic] here! ITYM incompleteness theorems. http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_the...