>> 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.
> I disagree ...
This is not a topic open to debate, it is a statement of fact. I strongly recommend that you learn this topic, and the topics of mathematics and logic, where some statements can be proven true or false without ambiguity.
The Turing Halting Problem applies to all Turing-complete environments. The program under discussion meets the criterion. AI meets the criterion. Lean meets the criterion.
> There are certainly definitions of non-trivial ...
This is a logical fallacy known as "Logic Chopping" : https://iep.utm.edu/fallacy/#Logic%Chopping
> where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.
Yes, I can see that, but that's not what this discussion is about. Read this before posting again: https://en.wikipedia.org/wiki/Halting_problem
Dozens of online articles on this topic, make the same point in the same way. None of them digress into logical fallacies.
> This may be something we cannot come to an agreement on morally ...
"Morally", really? Another logical fallacy, another digression, and not the topic.
> I disagree ...
This is not a topic open to debate, it is a statement of fact. I strongly recommend that you learn this topic, and the topics of mathematics and logic, where some statements can be proven true or false without ambiguity.
The Turing Halting Problem applies to all Turing-complete environments. The program under discussion meets the criterion. AI meets the criterion. Lean meets the criterion.
> There are certainly definitions of non-trivial ...
This is a logical fallacy known as "Logic Chopping" : https://iep.utm.edu/fallacy/#Logic%Chopping
> where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.
Yes, I can see that, but that's not what this discussion is about. Read this before posting again: https://en.wikipedia.org/wiki/Halting_problem
Dozens of online articles on this topic, make the same point in the same way. None of them digress into logical fallacies.
> This may be something we cannot come to an agreement on morally ...
"Morally", really? Another logical fallacy, another digression, and not the topic.