Isn't that the joke with Fermat's last theorem?

That he jotted in a margin that he had just seen a simple proof, and would write it down later. And we spent a hundred years trying to reproduce.

Or some other joke about a mathematician will put "and here we see it simply follows" or some such.

I'm all for abstraction, I get the point.

But for natural language it seems like " I saw my ex boyfriend last night and, yada yada yada, I'm really exhausted this morning".

See, the yada-yada is a bit too much abstraction.

I took the problem like this:

If we treat each human as a compiler of natural language, and there is enough ambiguity that each human arrives at a different result. Then is it really a proof?

Guess I'm missing the point of the paper, I thought it was trying to show that natural language is flawed and formalized systems are better.

And AI is getting tripped up by the human ambiguous natural language.