alt Hacker NewsThis is irrelevant. The theorems Avigard, Buzzard, et al. are talking about all have natural language proofs already that in theory should be formalizable.
They are not claiming all possible theorems are formalizable. They are claiming to try to formalize all already proven theorems in the mathematics canon.
To the extent the theorems in question are impossible to formalize this means the original proof must be in error.
Replies
netdevphoenix • today at 4:09 PM
Then, "All of Mathematics" is being used as clickbait.
>To the extent the theorems in question are impossible to formalize this means the original proof must be in error.
Theorems by definition must be formalizable. A theorem is not simply a true proposition, it's a provable proposition and a proof is necessarily a formal/syntactic property of a proposition.
That said, I agree with the sentiment that dismissing the entire article on the basis of the incompleteness theorems is shallow and the article is not about formalizing "all" of mathematics in the strict sense. It's mostly about introducing formal tools to the everyday mathematics.