Hacker News Reader

Hacker News

Comment by notrealyme123 | Hacker News Reader

Full thread

notrealyme123

I get the feeling a lot of people propose that we can write a verifier for every proof in lean.

Can someone tell me in simple terms why this doesn't conflict with the incompleteness theorems?

edit: thanks for the responses, i feel slightly less dumb now

View on HN

Well, I believe the incompleteness theorems speak about provability, not about how the proofs themselves are expressed.

We know as a consequence of Goedel theorems (at least I believe so), that there is no algorithm that would take a statement and output a proof if it is provable or a counterexample if it is not. However, AI provers never give anything for sure, so I think there is no contradiction here.

Not quite. If the statement is provable, an algorithm can find the proof by just looking at all possible proofs, in order of length. (It's assumed that that a valid proof can be algorithmically confirmed to be valid - there's an algorithm that when given a purported proof will eventually output "valid" if it is in fact valid.) The algorithm will find a proof eventually, if there is one. If there is a (provable) counterexample, the algorithm will similarly eventually find that. What Goedel's incompleteness theorem says is that such a search algorithm may never terminate - never finding a proof, and never finding a counterexample.

(The algorithms described above are of course completely impractical, taking time exponential in the length of the proof (of theorem or counterexample).)

The incompleteness theorems state that every sufficiently complicated logic lets you construct a statement that is effectively "this statement has no proof," so either there exists true statements that lack proofs (incompleteness) or there exists false statements with proofs (incorrectness).

I've had discussions around this with theorem prover types (OPLSS, highly recommend for people who can take the two weeks off)

The sort of head canon for any of the automated proof systems is that lean saying a proof is correct is "if lean is correct then the proof is correct".

One can get the temptation to try and prove lean correctness with lean but I believe _that_ is impossible due to the incompleteness theory.

_But_ the discussions I had, everyone was kind of in agreement with the idea that you could continue to shrink down the "kernel" of lean with lean (or whatever proof system really) so that in the end the thing you have to trust is pretty small.

I think lean can verify it implements its own rules, but not that its own rules are sound (you can't prove a contradiction). If you are just prepared to trust that the rules are sound, then you would be able to trust leans implementation (if you had that Lean proof that it implements its own rules)

Just all the useful proofs. You can get arbitrarily more complicated and uninteresting theorem statements by making meta statements about the system you are doing proofs in. At some level the system can't answer questions about itself.

The incompleteness theorem says that there are statements which can be neither proven true nor false in a given axiomatic system. If there is a proof to write in lean, then the statement is already outside the bounds of incompleteness.

Reply on news.ycombinator.com