On: How to Formalize All of Mathematics

[bossyTeacher]

I didn't claim that they claimed to have done it. My point is that you cannot do it.

You cannot formalize ALL of mathematics. We have known that for a while. Hence my point about the title being clickbait.

[Silamoth → bossyTeacher]

At best that seems like a nitpick based on a specific notion of “all of mathematics”. Care to explain what you mean?

[lioeters → Silamoth]

The title is intentionally misleading because the authors know all of mathematics is not possible to formalize, strictly speaking. And strict meaning is what math is all about.

[kevinbuzzard → lioeters]

Would you have been happier if we had called it "...all known mathematics"? This is what we are plainly talking about. The question we attempt to address is how best to digitise the corpus of known mathematics.

[bossyTeacher → kevinbuzzard]

Would still have been wrong.