Comment by notrealyme123
6 hours ago
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
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.
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).
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.