logoalt Hacker News

fwip • today at 2:59 AM • 1 reply • view on HN

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.

Replies

tristanj • today at 3:26 AM

The timeline here does not support your argument. Quoting from Buckmaster's statement:

  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.
Specifically: "For most of the past year progress was slow ... until about a month ago, when we had real progress: on August 15th"

And you avoided addressing the critical issue: they weren't even solving the same problem. Buckmaster solved a simplified and easier version of Navier-Stokes. OpenAI solved a harder version eligible for the Millennium prize. Buckmaster did not.

➕ show 2 replies