Comment by coafos
1 day ago
The same JavaScript code compiles to different machine representations under different browser engines; yet webdevelopers don't need to learn assembly.
There is an abstract javascript machine which can obviously be translated to hardware instructions. "Obvious" in the mathematical research sense, as in the statement is flat out wrong under closer inspection. Websites regularly crash under memory pressure.
But they are good enough most of the time, and that's the key. With more resource a more correct program can be created, but cost-benefit calculations show a ceiling. A local pet store does not have the money to pay 2000 hours of formal verification work, and usually a WordPress site is good enough.
Mathematicians work with their brains. They have finite time to understand papers. Formalists say that all theorems could be reduced to logical axioms, but most of time it's jumping at a much higher level, because no one has time for minute details. Proofs are theoretically right or wrong, but in practice there are "slightly wrong" proofs, where there are some minute errors that "feels" like can be correcte, and most of the time it can be. This ambiguity is not a problem, but a feature of mathematics, because it means more time can be spent to move faster at a higher level of abstraction, but this would be lost with Lean.
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.