> I want people to stop pretending they are surprised when the computer does exactly what it's instructed to do.
This is very wrong though. We now have many examples of cases where the computer very much does not do what it is instructed.
OpenAI's hack of DseWiki is an example where the instruction given to the AI agents was to collate data to generate economic reports and it hacked into DseWiki as part of that. It was not given instructions to do any sort of cybersecurity stuff.
The hospital bed stat research project was a similar thing, where OAI's AI agent found the hospital bed statistics through a simple web search and then hacked into the website anyways to download even more data.
More prosaically, models make up reasons for doing crazy things all the time!
Models may or may not be "malicious" (if that's even coherent), but at this point we have lots of evidence they definitely go off the rails in systematic, sustained ways that cause real world disruption that are not at all what they were instructed to do.
Models don't make up reasons for anything. They leverage their training data while running in poorly secured sandboxes often within the context of literal "hack/find a way/exploit" prompt by the labs themselves.
I don't think OpenAI ever actually disclosed what they were doing when the hijiacking happened. Probably because their previous stories like HuggingFace were all "oh, actually we were literally prompting agents to run hacking benchmarks in a poorly secured sandbox"
As I mention elsewhere (https://bugs.php.net/bug.php?id=78876) I'm very confused. Looking at the PHP bug tracker the specific bugs were fixed. So my best guess is that the LLM was able to find alternative variants that still worked? But then the report makes less sense.
> Looking at the PHP bug tracker the specific bugs were fixed. So my best guess is that the LLM was able to find alternative variants that still worked?
In the link from the comment to which you replied, buried deep below the comic strips and all that, there is this explanation which seems to confirm your guess:
> Right. We should explain from the start. My first step of finding if any long-lost siblings of Stefan's 2004 bug were still lingering in the codebase was to look for ways to exceed the memory_limit that allows us to throw a controllable fatal. I asked my LLM companion for help.
> The first useful finding was a way to bypass the smaller post_max_size barrier that normally prevents a request from delivering enough memory pressure to reach memory_limit. PHP compares post_max_size with the declared Content-Length before automatic POST parsing begins, but it does not enforce the same limit against the bytes it actually consumes. Apache can therefore pass a chunked HTTP/1.1 or lengthless HTTP/2 multipart request with no meaningful declared length. A configured input-decompression filter creates the same mismatch between the compressed length and the decoded stream.
> The second useful finding was a way to exhaust memory_limit with a multipart request that remains below post_max_size. An RFC1867 file-upload part with filename="" contains no file data, and PHP does not count it toward max_file_uploads. PHP still creates all six corresponding $_FILES entries: name, full_path, type, tmp_name, error, and size.
That report describes sending a 2^31 length filename, which is cast to a negative number, which leads to asking erealloc() to allocate a very large buffer, which fails, which leads to the symptoms of the bug we're discussing today (mid-request allocation failure becomes a partially initialised request)
The fix at the time wasn't to do proper cleanup on eralloc() failure, it was merely to avoid filename length being cast to a negative number.
> since Google showed you don't need to retrain an autoregressive model to rework it for diffusion inference
IIRC you do need to retrain the model, just closer to the level of finetuning rather than e.g. pretraining from scratch. Which also means that the model will perform differently with a different capability profile.
This 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.
>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.
> 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.
Yes that's fair. To be accurate the formal definition of a theorem entails that provability. I was being too loose in essentially using "theorem" to refer to any proposition.
There's maybe an even simpler way of illustrating this.
Fermat's Last Theorem is very easy to state. There are no positive integers a, b, and c such that a^n + b^n = c^n. This likewise easy to write in Lean. The statement of the theorem is exactly one line of code.
theorem fermat_last_theorem (n : ℕ) (n_ge_3 : 3 ≤ n) (a b c : ℕ) (a_is_positive : 0 < a) (b_is_positive : 0 < b) (c_is_positive : 0 < c) : a ^ n + b ^ n ≠ c ^ n
Kevin Buzzard's team of human mathematicians attempted to prove this in Lean. They got to about 60000 lines of Lean code and were not anywhere close to finishing the job.
Anthropic came around with a Claude model that proved it in 13 million lines of code. (Buzzard's team might have ultimately used within the same order of magnitude if they finished. It's very unclear. They were at minimum years away.)
Whether 60000 or 13 million, only one line of code was necessary to manually verify whether they had successfully proved Fermat's Last Theorem, just the statement of `fermat_last_theorem`. None of the rest of the code built up the theory at all.
Indeed if those lines of code built up the theory, that would suggest that the statement of Fermat's Last Theorem is incomprehensible, if professional mathematicians cannot define Fermat's Last Theorem in even 60000 lines of code! But that's pretty absurd. You can explain the statement of Fermat's Last Theorem, completely rigorously, to a middle schooler.
> First, one question arises: what are the 12 million lines doing if they're not needed? Secondly, don't those 12 million lines build up the theory that is eventually proved? Mistakes could be there that makes the outer statement seem like something it isn't, could there not be?
This seems to reflect an incorrect understanding of formal mathematics.
Formal mathematics can be thought of as a game with rules where a statement to be proved is some game end state. If you play 12 million valid moves and arrive at the desired end state then you have proved that the statement is valid. If your logical system is sound (e.g. first order logic), then you have proved your statement is true.
The entire point of the formalization of logic and mathematics through the 19th and 20th centuries was to unlock this capability. Such that, if you only care about whether your statement is true or not and not why it's true, the intermediate steps are entirely unnecessary.
To answer each of your questions:
> First, one question arises: what are the 12 million lines doing if they're not needed?
They are the intermediate computations necessary to show that the final statement is valid. This is much like intermediate arithmetic operations in a large complicated arithmetic expression. As long as you believe that the computer can calculate each individual arithmetic expression correctly, you don't need to manually review the billions of intermediate calculations that result in the final number.
> Secondly, don't those 12 million lines build up the theory that is eventually proved?
No. Not in the way you're thinking of. It seems you are using "theory" to mean the concepts necessary to express the statement itself. This is a very different set of lines than the proof itself (and generally much much more compact). Very difficult to prove statements can be stated in very simple language. Often the theory is <0.01% of the total lines of code.
> Mistakes could be there that makes the outer statement seem like something it isn't, could there not be?
No. Only the language used in the final statement can cause this issue, i.e. the theory. The intermediate 12 million lines cannot affect this, assuming your computer can carry out arithmetic correctly.
Another way of thinking about it is that the big breakthrough of 19th and 20th century mathematical logic is to conclusively show that formal mathematics is fundamentally just a set of arithmetic operations.
Hence in a very real sense, proving a mathematical statement is exactly identical to finding x in an arithmetic expression f with some constant k such that f(x) = k, where k is determined by the statement you wish to prove (not the 12 million lines).
Showing that x causes f(x) to equal k is exactly equivalent to proving the mathematical statement associated with k.
The 12 million lines are an alternative notation, no different in spirit to decimal notation or binary notation, of writing down x. It is some gigantic natural number.
You must understand k. If you use the wrong k, then you have proved another statement than what you intended. This is usually about a dozen lines of code.
You must be confident in the correctness of f. This corresponds to the believing that your type checker (since Lean uses dependent typing as its method of proof checking) has no fundamental soundness bugs. This can be controversial and indeed Lean's type checker has had soundness bugs in the past! But crucially f does not depend on k or x. Every time you fix a bug in f you can rerun it for any k or x you care about.
But you don't have to actually read all the digits of x, in whatever notation you care about. You can copy paste it in from some gigantic file handed to you by a stranger. As long as f(x) = k, you know that you have proved the mathematical statement associated with k.
Overall, this is roughly like asking why you trust a computer to solve a long division problem that has 12 million intermediate steps if you don't actually read all 12 million intermediate steps yourself. Well I trust the computer to do one step of division correctly and to be able to repeat that faithfully 12 million times. Hence I trust the computer can solve a long division problem involving millions of digits, even if I don't actually look at all 12 million intermediate computations myself.
> and that training data will not be a "new thing", because AI can't invent new things. Just recycling of what it already "knows".
Regardless of the truth of the underlying assertion, this is about as textbook an example of circular logic as it gets. (at least combined with the implicit beginning assertion that "AI can't invent new things.")
This is very wrong though. We now have many examples of cases where the computer very much does not do what it is instructed.
OpenAI's hack of DseWiki is an example where the instruction given to the AI agents was to collate data to generate economic reports and it hacked into DseWiki as part of that. It was not given instructions to do any sort of cybersecurity stuff.
The hospital bed stat research project was a similar thing, where OAI's AI agent found the hospital bed statistics through a simple web search and then hacked into the website anyways to download even more data.
More prosaically, models make up reasons for doing crazy things all the time!
Models may or may not be "malicious" (if that's even coherent), but at this point we have lots of evidence they definitely go off the rails in systematic, sustained ways that cause real world disruption that are not at all what they were instructed to do.
reply