151–158 of 158 posts
It's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it). To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?
Earlier quoted context omitted.
Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people wo…
It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved. This is the timeline: On June 29, Buckmaster opted out of model training, and stopped allowing his chats to be used as training data with OpenAI https://mastodon.social/@tristanbuckmaster/11723341370570119...…
It takes a lot of time to finish a proof and figure out the best way to present it. I would personally be surprised if Buckmaster had not gotten it mostly cracked before June 29th.
It's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it). To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?
Verification is also open ended (not sure about lean specifically) - you could in theory give lean just the Navier-Stokes problem definition to an ATP and let it run.
Earlier quoted context omitted.
It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved. This is the timeline: On June 29, Buckmaster opted out of model training, and stopped allowing his chats to be used as training data with OpenAI https://mastodon.social/@tristanbuckmaster/11723341370570119...…
I’m unsure or not if this is true but I did see some people saying that that checkbox when off only anonymizes your data, but it still may be trained on. Someone correct me if I am wrong
Earlier quoted context omitted.
It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved. This is the timeline: On June 29, Buckmaster opted out of model training, and stopped allowing his chats to be used as training data with OpenAI https://mastodon.social/@tristanbuckmaster/11723341370570119...…
> And OpenAI directly addressed these plagiarism claims, and called them impossible Funny, you were telling me two days ago that on the contrary, "it’s genuinely impossible to know how much of Buckmaster’s Codex data is in OpenAI’s training set": https://news.ycombinator.com/item?id=49621648
It's practically impossible to know how much of Buckmaster's pre-June 29 data persists in OpenAI's systems. That includes all chats (which are anonymized), any (thumbs up/thumbs down) chat ratings used as RLHF feedback (which are anonymized), any synthetic data derived from said anonymized chats and RLHF feedback, and any downstream models derived from said synthetic data.
Buckmaster’s Codex data from prior to June 29 has been completely laundered, in the same way as a crypto mixer.
Earlier quoted context omitted.
It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved. This is the timeline: On June 29, Buckmaster opted out of model training, and stopped allowing his chats to be used as training data with OpenAI https://mastodon.social/@tristanbuckmaster/11723341370570119...…
It doesn't seem like you're familiar with how mathematical research is done. Taking 6 weeks between a major breakthrough on a huge proof, and making your proof public, is not unusual. It takes a lot of time to finish a proof and figure out the best way to present it. I would personally be surprised if Buckmaster had not gotten it mostly cracked before June 29th.
For most of the past year progress was slow. We worked through the literature and upgraded various preliminary results, up to obtaining finite time blow up for the Incompressible Porous Media equation (with smooth forcing). This was until about a month ago, when we had real progress: on August 15th, we obtained the blow up results, with smooth forcing, for both Boussinesq and Euler.
I can say the first LLM generated proof Levent sent me was the most horrendous I have ever read; we verified it on Lean on August 22nd. Since this point, we have been working around the clock to understand this proof and turn it into something readable.
And you avoided addressing the critical issue: they weren't even solving the same problem. Buckmaster solved a simplified and easier version of the problem. OpenAI solved a harder version eligible for the Millennium prize. Buckmaster did not.
IMO the "forty hours per page" rule is not up to date, and more a consequence of lacking proof automation in 2005. From what I understand about Lean, this has been one of the things that they have put a lot of effort into improving, making proof mechanization more palatable to the mathematically inclined, as opposed to just logicians.
Earlier quoted context omitted.
> Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers It's also true however that I haven't seen a single write up trying to discern what did more of the work in those AI chats - the prompts or the responses - bubble to the surface, also since we don't have access to them. For example, if I prompt Codex with "Make me a…
The researchers apparently spend a year or so working on this, and it builds off significant previous work, so it seems like it was a pretty significant amount of work that OpenAI may have trained on I'd love to see an in depth analysis of how much OpenAI actually did, but I suspect we'll never see that because it would indicate at least some plagiarism which undermines a lot of what OpenAI is putting out in public
This is a good summary:
> In broad outline, the pair’s technique relies on creating an infinite sequence of “layers,” each of which is a non-singular solution to the equation they are studying. (They’ve applied similar techniques to both the Euler and Navier-Stokes equations, as well as to other related systems.) They then combine those solutions in what Martínez-Zoroa calls an “infinite cascade” to produce a new solution. > > That new solution, they showed, contains the desired singularity. However, even though each individual layer relies on a smooth forcing function, combining them together can cause the forcing function to have undesirable mathematical properties. That’s why their solution fell short of satisfying the Millennium Prize criteria. The remaining hurdle was to figure out how to create a similar infinite cascade that resulted not only in a singularity, but also in a smooth forcing function. > > That’s the step that both competing AI groups appear to have had success with.
https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-...
The question is whether OpenAI started out from that published and well known research exclusively, or they also had some insight into the ongoing work of Tristan Buckmaster and Levent Alpöge.
On the one hand, OpenAI have already admitted that they only launched their massive effort after hearing rumours that this particular problem had been solved.
On the other, progress in mathematics research has accelerated significantly over the past months thanks to the availability of newer and more capable AI models. Alpöge himself presented a counterexample to the Jacobian conjecture on July, found with Claude Fable. So if model capability was a bottleneck, that gives credibility to the idea that an even more powerful unreleased model with massive compute would be able to make even faster progress.