Can Computers Prove Theorems? • Hacker News Board

Re: Can Computers Prove Theorems?

#11

Post by phonebucket » Thu, Oct 31, 2019, 11:52 AM UTC

tom_mellior wrote: post #8

phonebucket wrote: post #6

Lean has been going hard at PR at the moment. I would really like to dip my toe into the theorem proving waters from a scientific/mathematical perspective. I'm not sure whether to start with Coq, Agda, Isabelle or Lean. Does anyone on HN have a feeling as to a sensible one to start with?

Start with the one with the best documentation. It's hard to beat Software Foundations: https://softwarefoundations.cis.upenn.edu/ , which happens to be for Coq. If you search the web for "Software Foundations in X", you will find partial ports of some of the initial chapters to pretty much any other proof assistant. Maybe nowadays they are full, complete ones that would allow you to use Isabelle or Lean instead.

Software Foundation and Coq looks like a fantastic resource. Thank you very much.

Re: Can Computers Prove Theorems?

#12

Post by mannykannot » Thu, Oct 31, 2019, 12:03 PM UTC

"However, if computers do get better than humans at proving theorems, I might be out of a job anyway."

Not until computers are coming up with useful axiom-sets and effective tactics, I suppose.

Re: Can Computers Prove Theorems?

#13

Post by thanatropism » Thu, Oct 31, 2019, 12:04 PM UTC

Jean-Yves Girard says that true theorems have corollaries.

Computers can prove all sorts of propositions, but the gooey philosophical question is -- which propositions are Theorems in the grand civilizational project of mathematics?

Re: Can Computers Prove Theorems?

#14

Post by DailyHN » Thu, Oct 31, 2019, 12:04 PM UTC

If this is interesting to you, I recommend "The Book of Why" by Judea Pearl.

Re: Can Computers Prove Theorems?

#15

Post by black_knight » Thu, Oct 31, 2019, 12:11 PM UTC

Yajirobe wrote: post #9

ctrl+F Gödel ctrl+w

Gödel’s incompleteness theorems are actually not very relevant to computer formalisation of mathematics. They crushed the naïve hopes of some classical logicians in the beginning of the 20th century. But they do not pose any further restrictions on what computer can do, as opposed to what a human can do, with any specific set of axioms.

Re: Can Computers Prove Theorems?

#16

Post by arethuza » Thu, Oct 31, 2019, 12:15 PM UTC

thanatropism wrote: post #13

Jean-Yves Girard says that true theorems have corollaries. Computers can prove all sorts of propositions , but the gooey philosophical question is -- which propositions are Theorems in the grand civilizational project of mathematics?

So software can mechanically crank through and generate propositions but which of these are actually worth paying attention to?

Edit: Has anyone tried deep learning (or similar techniques) to do the identification of interesting theorems?

Re: Can Computers Prove Theorems?

#17

Post by black_knight » Thu, Oct 31, 2019, 12:15 PM UTC

thanatropism wrote: post #13

Jean-Yves Girard says that true theorems have corollaries. Computers can prove all sorts of propositions , but the gooey philosophical question is -- which propositions are Theorems in the grand civilizational project of mathematics?

Yes, the job of a mathematician is not to prove theorems. But rather to find the interesting or beautiful ones.

Re: Can Computers Prove Theorems?

#18

Post by fnrslvr » Thu, Oct 31, 2019, 12:32 PM UTC

Yajirobe wrote: post #9

ctrl+F Gödel ctrl+w

If the headline question were something more like "can computers prove all theorems reliably?" this response would be more understandable. But a fairer interpretation would be "do automated theorem proving techniques stand a chance of making novel contributions to the mathematical literature?", to which I think it's pretty unfairly dismissive to rule out the possibility at this point. Considering it's still pretty early days for automated theorem proving, there's already some promising progress: an automated prover resolved the Robbins conjecture.

If you think Gödel's incompleteness theorems are hard evidence that computers can never consistently perform on the same level as humans at theorem proving, take it from someone who understands Gödel's results well: you're mistaken.

---

I think one sense in which the headline seems a little misleading, though, is that on a skim it looks like it's more about formalizing mathematical knowledge so that computers can verify theorems proven largely by people, than it is about computers themselves proving the theorems. (Which is also a fine topic, I'm not complaining.)

Re: Can Computers Prove Theorems?

#19

Post by tel » Thu, Oct 31, 2019, 1:23 PM UTC

The title is a bit misleading. The author doesn't really discuss whether computers can perform the act of proving. He's mostly focused on whether computer languages can represent proofs (yes) and whether computers can check them (yes).

Computer can also search for theorems and proofs to those plausible theorems. There are issues, of course. Both of these spaces are very, very large. It's not clear what makes for an "interesting" theorem to prove.

Proof through proof search is also semi-deterministic in that the search will continue until it finds an answer. If the search hasn't terminated yet, it's either because there is no proof or because it just hasn't worked hard enough... yet.

You could conceivably "race" searches between P and (not P) and hope that this would save you since now one of the two will return in finite time. Unfortunately, most of these proving languages are constructive and thus it's possible for both of those to be unprovable.

It's all very cool, but we're still not getting close to having computers realistically "prove" things of interest.

Edit: Worth also noting quickly that proof search is used pretty regularly in these systems, but it's a sort of localized, partial, and interactive proof search where "tactics" for the search are human specified or search is used as an interactive tool for skipping over "boring" parts of proof construction.

Re: Can Computers Prove Theorems?

#20

Post by tel » Thu, Oct 31, 2019, 1:25 PM UTC

phonebucket wrote: post #6

Lean has been going hard at PR at the moment. I would really like to dip my toe into the theorem proving waters from a scientific/mathematical perspective. I'm not sure whether to start with Coq, Agda, Isabelle or Lean. Does anyone on HN have a feeling as to a sensible one to start with?

Coq is definitely the best documented. Unfortunately, the tendency to use the tactics language—while incredibly practically useful—obscures how the structure of proofs relate to their theorems.

This isn't really a problem per se, but instead an invitation to look into, say, Agda to see that side of things, too.