> It blocks AI mistakes, it only accepts ones able to be proven.
This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
> It might also be prudent to ask the author if they really mean they interpretation you take
How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.
> What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim?
I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .
This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
> It might also be prudent to ask the author if they really mean they interpretation you take
How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.
> What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim?
I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .