Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Can Computers Prove Theorems?

chalkdustmagazine.com

Post reply on HN
Print view View original

41–50 of 61 posts

Re: Can Computers Prove Theorems?

#41

Post by eli_gottlieb »

mcguire wrote: post #38

" 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-as…

I'd be very curious to know, empirically, whether people who aren't trained in computer science, software engineering, or pure mathematics consider reading a proof or reading a program to be easier and more understandable.

Re: Can Computers Prove Theorems?

#42

Post by derefr »

mcguire wrote: post #38

" 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-as…

Humans like to pretend business-logic workflow digraphs are actually workflow trees. Every programming language† is an attempt to "tell the story" of the runtime paths through a digraph of control-flow, using a lexical tree of syntax structures. I've only written a few proofs in my life, but I get the sense that "at scale", they're quite similar: a narrativization or expiation of a bunch of paths through lemma-space, that branch out and re-converge.

When any program becomes sufficiently complex, its nature as a digraph is forced to the surface, and the ability to continue to pretend it's just a tree becomes untenable. We get confused, working with these complex digraphs, unless we use tools that allow us to visualize digraphs as digraphs, walking around them and looking at them from different angles.

Honestly, I don't think this is anything to do with "doing programming [or proof-writing] wrong", so much as it is an inherent fact of the nature of systems of lemmas. It's a bit like how humans can't visualize hypercubes directly—we need to instead use a tool (lower-dimensional projection) to "walk around" these mathematical objects and look at them from different angles, in order to understand them. I would posit that systems of lemmas are just such a mathematical object.

Sure, you can try to find isomorphic programs, or proofs, that are more lexical-tree-like, and so easier for humans to hold in their heads. But if you require that your programs, or proofs, fit to some standard of tree-like-ness, there'll be some programs/proofs that you just won't be able to write. Maybe that's not so bad for programs (those programs were probably awful anyway), but ignoring a proof (or an area of proof-space) when it's perfectly valid, just because we need tools to look at it, seems a bit silly.

---

† Or rather, every programming language that people use in practice, because even in languages with GOTO, people avoid it, and restrict themselves to the structured-programming subset of the language. The programmer who wants to write everything as coroutines or (call/cc)s is pretty rare.

Re: Can Computers Prove Theorems?

#43

Post by drdeca »

black_knight wrote: post #26
tel wrote: post #19

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 "…

> Unfortunately, most of these proving languages are constructive and thus it's possible for both of those to be unprovable. The fact that it is possible for a given proposition P to be neither provable nor disprovable has nothing to do constructive mathematics. This happens in classical mathematics as well – in any incomplete theory. All theories which serve as foundation of mathematics are incomplete (ref. Gödel).…

I was going to say "what if you look for a proof of (¬¬P)∨(¬P)" , but, to my surprise, apparently that is also not a tautology in intuitionistic logic? So, I knew that ¬¬(P ∨ ¬P) is a tautology in intuitionistic logic, but, to my surprise, (¬¬P)∨(¬P) is not.

Here is a twitter bot that evaluates whether statements are tautologies in intuitionistic logic, and it gives the answer that (¬¬P)∨(¬P) is not, and gives a "kripke counterexample" https://twitter.com/ipc_bot/status/1189953697486229504?s=20

Mentioning this because I was going to respond by saying "but isn't (¬¬P)∨(¬P) still a tautology? Then, how does intuitionistic logic / constructive logic, help with avoiding the problem?", but then I checked, and was surprised, so I thought other people might have the same misconception I had, so I'm saying this.

However, if (P is provable in classical logic)∨((¬P) is provable in classical logic), doesn't it follow that either ((¬¬P) is provable in intuitionistic logic) or ((¬P) is provable in intuitionistic logic) ?

Re: Can Computers Prove Theorems?

#44

Post by xvilka »

Yes, it's already possible[1] with Coq. There are two strategies for that - lowering the CIC (Calculus of Inductive Constructions) to SMT[2] and employ SMT solvers like Z3, and employing Deep Learning[3][4]. For the Lean part, compared to Coq - there is an interesting discussion[5] why Lean might be not as good as they claim.

[1] https://coq.discourse.group/t/machine-learning-and-hammers-f...

[2] https://github.com/lukaszcz/coqhammer

[3] https://arxiv.org/abs/1907.07794

[4] https://github.com/UCSD-PL/proverbot9001

[5] https://github.com/coq/coq/issues/10871

Re: Can Computers Prove Theorems?

#45

Post by drdeca »

yters wrote: post #32

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.

Is the problem with finding the Gödel sentence, or with proving it?

I believe the issue is the proving it.

For a sentence to be a Gödel sentence of something, that something, I think, should be a formal system, a set of inference rules and axioms. While there may generally not be much issue in talking about "the Gödel sentence of [a process/thing that uses such a system]" to refer to the Gödel sentence of the system that the thing uses, in this case, I think there is no issue. Finding the Gödel sentence of a system is, iirc, a fairly straightforward computational process, given a good description of the system.

So, it should be no difficulty to have a program that takes its definition of a system, and checks proofs in that system / looks for proofs in that system, and also computes the Gödel sentence of that system.

Furthermore, I think (but am slightly less sure, though still fairly sure) that consistent and sound systems can prove things like "if the system [description of self goes here] can prove [Gödel sentence of the system], then it is not consistent." .

Furthermore, I see nothing establishing that humans can do any better than computers in this regard.

Be careful when using the Gödel incompleteness theorems as justifications of positions! They are often misinterpreted.

Re: Can Computers Prove Theorems?

#46

Post by 3PS »

> Occasionally we mathematicians find that we need a new tactic—for example proving that (a+b)^3=a^3+3a^2b+3ab^2+b^3 just from the axioms of a ring is surprisingly difficult!

Perhaps because what you need there is not just a ring, but a commutative ring :P

Jokes aside, that was an excellent article and introduction to interactive theorem proving. I'm looking forward to seeing what Lean 4 brings to the table when it's released.

Re: Can Computers Prove Theorems?

#47

Post by nocturnial »

This article is about lean and I really like and want to like lean. But... At the moment it bothers me that the authors still consider it an experimental engine. In this case it means development stopped on version 3 when they started version 4. No bugfixes, no enhancements are accepted into version 3.

When/if they make the mental switch from experimental to a supported product, I'll definitely use it and maybe even contribute to their proof library (if there are low hanging fruits left).

Re: Can Computers Prove Theorems?

#48

Post by infogulch »

agentultra wrote: post #25

Lean is also a really, really good dependently typed functional programming language. If you're on the software developer/computer science side of the coin I highly recommend looking into it. It's not only for maths research (although that is definitely a big focus of the majority of the Lean community). I'm working on a forthcoming series of blog posts investigating FP concepts from scratch in Lean to see how it tak…

How does Prolog relate to more formal languages like Lean/Coq? Prolog (pretty easily) has dependent types [1] as well. Is there something in the language itself that would make it unsuitable as a theorem prover, or is there something it's missing? I'm trying to get a feel for Lean from the vantage of a bit of familiarity with Prolog.

[1]: https://llaisdy.co.uk/2014/05/07/dependent-types-in-prolog/

Re: Can Computers Prove Theorems?

#49

Post by solveit »

eli_gottlieb wrote: post #41
mcguire wrote: post #38

" 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-as…

I'd be very curious to know, empirically, whether people who aren't trained in computer science, software engineering, or pure mathematics consider reading a proof or reading a program to be easier and more understandable.

I would guess that they bad enough at both that the difference doesn't really matter. I would be interested in what someone at the highest levels of all three fields thought, but I'm not sure these people exist.

Re: Can Computers Prove Theorems?

#50

Post by agentultra »

infogulch wrote: post #48
agentultra wrote: post #25

Lean is also a really, really good dependently typed functional programming language. If you're on the software developer/computer science side of the coin I highly recommend looking into it. It's not only for maths research (although that is definitely a big focus of the majority of the Lean community). I'm working on a forthcoming series of blog posts investigating FP concepts from scratch in Lean to see how it tak…

How does Prolog relate to more formal languages like Lean/Coq? Prolog (pretty easily) has dependent types [1] as well. Is there something in the language itself that would make it unsuitable as a theorem prover, or is there something it's missing? I'm trying to get a feel for Lean from the vantage of a bit of familiarity with Prolog. [1]: https://llaisdy.co.uk/2014/05/07/dependent-types-in-prolog/

I'm not sure I can answer that question. I don't know enough about Prolog. I can say that your example could be encoded in Lean as a type and the definition would probably be much shorter.

Does Prolog automate some of the work involved in writing a proof?

Post reply on HN