Comment by skywalqer
12 hours ago
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).)