Can Computers Prove Theorems? • Hacker News Board

Re: Can Computers Prove Theorems?

#31

Post by [deleted] » Thu, Oct 31, 2019, 3:15 PM UTC

tel wrote: post #20

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.

[deleted]

Re: Can Computers Prove Theorems?

#32

Post by yters » Thu, Oct 31, 2019, 3:53 PM UTC

Can computers solve the halting problem? If not, then they cannot find their own Godel sentence, and thus are limited in their ability to prove things.

Re: Can Computers Prove Theorems?

#33

Post by segfaultbuserr » Thu, Oct 31, 2019, 3:53 PM UTC

For (some) much simpler first-order logic systems, the answer is certainly true. Tarski's axioms imply that there exists an algorithm that, for every proposition in (a restricted) Euclidean geometry, can be shown either true or false.

Re: Can Computers Prove Theorems?

#34

Post by vilhelm_s » Thu, Oct 31, 2019, 4:08 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 and Isabelle are much more mature systems, they have already been used in a lot of big developments, and they have large user communities and existing textbooks and so on.

Agda is pretty finicky, proving stuff in it is harder and the entire project feels more researchy (as a playground to try out ideas for programming languages).

Lean seems promising, but it's still kind of new, so compared to Coq will not find as much documentation, and there are fewer people on Stack Overflow to answer questions.

Re: Can Computers Prove Theorems?

#35

Post by RedComet » Thu, Oct 31, 2019, 4:10 PM UTC

You can axiomatize anything. The axioms are chosen because they reflect reality. The axiom reflects the blocks, not the other way around.

Re: Can Computers Prove Theorems?

#36

Post by dwheeler » Thu, Oct 31, 2019, 4:12 PM UTC

Computers can directly prove some theorems today, and in other cases there are various interactive provers that let humans and computers work together to find formal proofs. In some systems using computers can give much better confidence that the proof is correct, because computers are very good at carefully checking every step; nitpicking is their forte and they don't get tired.

Freek Wiedijk maintains a list of 100 challenges for math formalization and the status of various systems here:

http://www.cs.ru.nl/~freek/100/ - Formalizing 100 Theorems

Lean hasn't accomplished as many as some others, but it's certainly a contender!

Re: Can Computers Prove Theorems?

#37

Post by zozbot234 » Thu, Oct 31, 2019, 4:22 PM UTC

tel wrote: post #20

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.

Agda just uses proof terms directly - you could do that in Coq and Lean as well. It's a bit of a bummer though that neither Coq nor Lean have a currently-maintained declarative mode ala Mizar/Isar. The former C-zar included in older Coq versions (aka Mathematical Proof Mode) was especially nifty, albeit not totally free from bugs.

(One other approach is to generate a "declarative", human-readable version of the proof directly from the proof term. Very old versions of Coq (6.x series) and IIRC even Agda (1.x) could essentially do this. Declarative proof mode integrates better with complex tactics however - proof terms can sometimes get a bit weird.)

Re: Can Computers Prove Theorems?

#38

Post by mcguire » Thu, Oct 31, 2019, 4:38 PM UTC

"This is the last Lean proof which I will give here. The reason is that for proofs any more complex than this, it gets hard to follow them on paper. The way to understand these proofs best is to look at them in Lean itself. If a proof were running in Lean on a computer then you could click anywhere on the proof and see Lean’s state (what it knows and what it is trying to prove)."

Yeah, there's the problem: Proof-assistant produced proofs are difficult to read as proofs. The alternatives are to execute them, as you would execute a program in a debugger to understand it (um, ick), or to "pretend to be the computer" and execute them manually.

The interesting part is that exactly that problem is faced with software, which developed ways of writing programs that are easier to understand, including using formal methods.

Re: Can Computers Prove Theorems?

#39

Post by drdeca » Thu, Oct 31, 2019, 4:58 PM UTC

not_a_math wrote: post #24

We have a bunch of theorem provers - Lean, Coq, Agda, Isabelle If you prove something in Lean, can you automatically convert the proof into a Coq one (even if it looks like uglyfied/minified code)? It feels like it should be possible to "merge" the proof repositories of these languages together into a common one. Or to put another way, if you can prove in Coq that Lean is correct, then it should imply that Lean proof…

I asked a similar question in the comments on a youtube video, and Mario Carneiro, one of the people who work on Lean, answered me.

He said he does work on this area, and it kind of works (at least for the theorems you would want to translate?), but in addition to the proofs being very not nice to read, the way the statements of the theorems are translated are, by default, also rather not nice (being statements about specific formulations of the objects (such as the set of integers) as they are expressed/defined in the language being translated from, instead of referring to the corresponding objects that have been defined in the language being translated to. However, he says that it doesn’t take all that much work to manually massage it until the statement of the theorem is expressed in the way that you want it to be.

I’m on my phone right now, and the phone youtube app doesn’t give me a permalink, but I’ll try and edit this comment soon on laptop to include link to the comment section.

Edit : here are links to what Mario Carneiro said in the thread click the read all replies to read the full thread)

https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S...

Re: Can Computers Prove Theorems?

#40

Post by devinplatt » Thu, Oct 31, 2019, 5:02 PM UTC

Laakeri wrote: post #21

black_knight wrote: post #17

Earlier quoted context omitted.

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

However currently the most difficult and time consuming part of the job is proving those interesting theorems.

I'm genuinely curious, why do you believe this? From experience? From hearing mathematicians say so?

I'm currently working on my first formal math paper, and I've been spending a lot of time figuring out how to best present the information so that it is comprehendible and easy to read. Things like structure of the paper, wording, notation, and more.

There's probably a lot of time to spend convincing others that your theorem is interesting, too. Some of the most respected works in mathematics after all are thoughtful compilations of previously proven results.