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.
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.
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?
[Citation needed]
2 + 2 = 5 -> Error
Every time.
The environment does matter. I think in your original objection, you were executing the code in different environments.
https://cs.stackexchange.com/questions/38152/what-is-determi...
And to the point of the original article. Each human interpreting natural language is a new environment. Each brain is a new compiler with different outcomes. Thus the ambiguity. Natural language isn't concrete enough to always have the same result when processed by different humans, or AI.
> the answer with many multi-threaded programs is often "no."
Isn't the original point, that natural language isn't sufficient for proofs? Aren't you agreeing now?
The point of the article is that natural language is not these things.
If you understand the Lean, then you can create a NL proof. The LLM clearly doesn't understand the Lean code it produced.