Posted by milkshakes 6 hours ago
Maybe good AI paper writing is further away than I thought...
I'd honestly rather they just automate every job at that point.
> We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness
Offering to take responsibility for the correctness of a proof written in Lean feels like volunteering to be the fall guy in case someone finds a flaw in basic arithmetic, no?
I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications), that the lean proofs are checked against, indeed correctly encode the real theorems. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
As I currently understand it, all we know is that:
- a mathematician produced a Lean-verified counterexample to the Collatz conjecture, demonstrating a bug in the kernel
- he claims that LLMs were involved somehow but pointedly refuses to specify how
- he admits that he knew about the bug before publishing the counterexample to his repository.
Perhaps not a joke (although it sure seems to me like they discovered a bug and thought falsely disproving the Collatz conjecture would be a flashy way to announce it), but at best extremely sensationalized by the above description. If you have additional context I would be happy to hear it!
Training the model is going to be amortized over other uses.
Say that it turned out that the total cost of the proof of the Erdős unit-distance conjecture was $50 million.
Then the question really becomes: yes, these models are capable of proving important mathematical results, but at a very high cost. Is it worth it?
If a mathematician applied for a research grant of $50M USD for proving the same thing, they would have been laughed out of the bank.
What's more is that when you have a research grant, you train PhDs and postdocs, you hire new staff, and you disseminate. That is, you get much more value for the money spent.
I'm just curious what the cost is.
Hours needed for prompt + Hours needed to check result + API costs.
You don't say "well let's add together the total yearly compensation of all the engineers and mathematicians at OpenAI that were involved" and throw that into the total cost. That's simply nonsense accounting.
The actual comparison you are making is some university researcher weighing between getting a grad student (several tens of thousands of dollars) vs typing up a prompt and sending a request to OpenAI for inference (as mentioned in the article, around $2000 in API and maybe a few hours for the prompt and harness).
Edit: Oh, are you suggesting they just use it to privately improve their models? I imagine a few more correct proofs would have a very marginal benefit, if any. Also, they'll probably just get extracted, meaning it still gets out but OpenAI doesn't get to fancily announce it themselves.
However, I was looking at the proofs and reason explanation and openAI should be more explicit in how the work has flown. I find the models have jumped hoops in some places of the proofs, that can be hard to track. In fact, when a paper is published you usually get a review and if no reviewer understands they ask you to further explain the thought process. It will be fun to see if this happens here.
[1] https://x.com/henryquantum/status/2083623695436623915?s=20
Which is very suggestive - if after everything they are not fully loaded then the next gazillion data centres being built look unlikely to be needed.
If anything it proves more data centres are needed. That's literally the only reasonable conclusion from this news.
Are you arguing there is not an AI bubble, and that all the DC buildout is fine, going to be profitable etc?
I am not looking for a online slanging match - just looking for a different point of view
I’m not participating in the slinging match but it’s very very weird that you think it’s some established thing that these companies won’t make profit. A lot of hubris must go in this kind of thought. Like.. do you all think everyone’s playing musical chairs?