traes

Perhaps out of a sense of academic good will, knowing that he got there first?

It seems like the timeline according to OpenAI is that:

1. Buckmaster developed a counterexample to a reduced version of Navier-Stokes with Anthropic employee Levent

2. Rumors start spreading that Anthropic has solved Navier-Stokes

3. OpenAI learns this and starts throwing a ridiculous amount of compute at it, now knowing it's within reach of LLMs

4. Their LLMs (with human assistance) get FARTHER than Buckmaster, using the exact same method.

5. OpenAI reaches out to Buckmaster to negotiate a fair way to publish both results and properly assign credit

Perhaps they simply and honestly feel he is owed credit. I can't help but imagine it at least played some small part. I expect that's what Bubeck is going to claim: https://xcancel.com/SebastienBubeck/status/20972141224714323...

Because OpenAI employees kept leaking that Anthropic had a solution to Navier-Stokes and he wanted to figure out what was going on, since he was working on Navier-Stokes with an Anthropic employee. The rumor has been loudly circling the math community for the past week or so. For a bit of context, here's a timeline from mathematician and AI researcher Elliot Glazer:

https://xcancel.com/ElliotGlazer/status/2096298696438906934#

The accused Sebastian Bubeck has denied the allegations on Twitter[0], and various other OpenAI employees[1,2] seem to be mocking another Anthropic employee voicing support for Levent[3]? Things are getting messy.

[0] https://xcancel.com/SebastienBubeck/status/20972141224714323...

[1] https://xcancel.com/polynoamial/status/2097215233119211902

[2] https://xcancel.com/danintheory/status/2097214838003138603

[3] https://xcancel.com/_sholtodouglas/status/209721833169057800...

To be clear, Astra played little part in Buckmaster and Alpoge's work:

> We used several LLMs throughout: Anthropic’s Claude, OpenAI’s Codex, especially with GPT-5.6 Sol and, more recently, Astra. The latter was only used for writeups and auditing our arguments.

No. From the paper linked above [0]:

> The phase of free fall is predicted in a purely quantum manner to have a dependence m/6 g^2T^3/ℏ + gmzT on the free-fall time T, where m is the mass of the object, g is the gravitational acceleration relative to the surface of Earth, and z in the spatial coordinate in the direction of gravity. This prediction follows the calculated phase accumulated by an object accelerating in a linear potential, and has been made starting from almost one hundred years ago by Darwin, Kennard and others.

Apparently the phase shift is derivable from just adding a linear potential term mgz to the Hamiltonian.

[0]: https://arxiv.org/pdf/2502.14535

Seems like they just added a linear gravitational potential term mgz to their hamiltonian and computed the phase change it would induce. They claim they experimentally confirmed the phase change. I didn't think that worked! They also claim its consistent with some kind of GR derivation, but I haven't looked at that.

The repo is public. You can just go look! It's really not that surprising; FLT is huge and has a ton of dependencies that need to be implemented, and there's a degree of sloppification that is probably blowing up the size by a few factors.

25-50 seems like a pretty lowball estimate, I guess depending on your definition of "understand."

We have absolutely no idea if this was a brilliant breakthrough or not. They haven't released any explanation of how it was found. A problem being old and prestigious does not mean its solution is automatically a brilliant breakthrough.

It's true that his goal was not the full thing, but it was also not merely a Lean verified proof. From the blog post linked in the toptext:

> The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof.

For clarity:

  The autumn wind moves slow across the field,
  and every falling leaf now yields its fight.
  The summer gold at last has ceased to yield,
  and short days now give way to longer night.
  I walk alone beside a calm and quiet stream,
  and watch it slowly carry every fallen leaf.
  I think of you as some half-forgotten dream,
  and taste again that same old, bitter grief.
  The silent stars come out to watch it still,
  and pale moonlight falls gently on the hill.
  A lonesome owl calls out from past the mill,
  and time moves on, unhurried and calm, until
  the dawn returns to paint the sky brand new,
  and I still recall the love I lost with you.

Completely off topic, but I really don't understand the demographic of physics educators that are resistant to Dirac notation in a first QM course. It isn't really that hard to explain or understand, it's extraordinarily convenient, and it's essential for engaging with most quantum adjacent literature. I understand that it conceals the distinction between vector space and dual space a bit but it's really not that hard to get through. I may be biased because I learned the notation in week 2 of intro quantum, so I am curious if anyone with the opposite experience disagrees.

The title should say (2022)

Very bold title! Turns are very convenient until you need to calculate a rate of change, as of course d/dx sin(2pi x) = 2pi cos(2pi x). Unfortunately this is a common enough problem that I will be sticking with the radian.

I think the volume explanation is one of the most intuitive pieces of math in existence, personally! Uninvertibility of a tranformation corresponds to a volume of zero because the transformation must squish two dimensions together, leaving them impossible to differentiate, det(AB) = det(A)det(B) because applying two transformations applies their scaling successively, det(A^-1) = 1/det(A) because you have to undo the scaling to invert a transformation etc. I don't think the permutation definition is even strictly necessary; if I recall correctly Linear Algebra Done Wrong defines the determinant in terms of its geometric definition and develops its formula from the properties it must have. I think that the concept is well worth the investment of initial confusion. Axler disagrees, however.

Note that "done right" means done with Axler's completely subjective and unusual hatred of determinants, chronicled here [0]. It is in no way "done right" in some definitive, rigorous way; most math professors I have spoken to either strongly disagree with the presentation or have no particular preference.

[0] https://www.axler.net/DwD.html

This polemic: Sheldon Axler -- Down With Determinants

https://www.axler.net/DwD.html

A strange and unpopular opinion.

There was no depth to mathematics in Euler's time, he made the depth. He arguably didn't understand analysis on a technical level as well as a modern undergraduate; as I recall, he was confident that all smooth functions are analytic. He had incredible intuition and was able to make great progress by trusting it, but playing around with tools you don't understand stops being effective once a field is past its infancy.

How fast do your monkeys type?

Proof verification can be done automatically via Lean (or similar), so the parallel breaks down unfortunately. The only thing humans really need to verify is the translation of the theorem statement and the correctness of the proof checker.

> If progress is stuck, the machine turns the gauge away from "exploit" and toward "explore"

It sounds like you've answered your own question of:

> why "pure mathematics" should persist as a field of human or machine activity.

And you're really just quibbling about scheduling.

Whether humans will be involved or not is an entirely different debate.

There's a substantial gap between "the machine is better than human mathematicians" and "the machine can formalize a solution to any problem immediately." Much of the important mathematical theory behind modern science was mapped out in advance by mathematicians, and scientists were able to find and take advantage of this mathematics where applicable. Mapping out our understanding of e.g. physics and our understanding of mathematics in parallel and finding connections later has historically been a highly successful approach, and I see no reason to believe the same would not be true for advanced machines. Would Einstein have been able to formulate GR without the existing theory of differential geometry? Maybe, but maybe not. Would an advanced machine be able to develop the theory of differential geometry in response to gravitational measurements? Maybe, but maybe not.

Edit: Perhaps I could have been terser here. Really the idea is that small jumps are easier to make than big jumps. Continually developing pure mathematics is a way to make small jumps in logic and intuition add up to big jumps in applications.

It's speculative fiction written by a professional mathematician about his idea of the worst case scenario of AI's effect on math.

Out of curiosity, what is the largest C program you have written pre-LLM, and did you ever try to run it through valgrind*? The "oversights" in C tend to be extremely subtle and dangerous, and of a type that would be impossible to make in Go (or Rust or Common Lisp or whatever.) I do not have confidence in LLMs not falling victim to these subtleties at least once in a large application. I could be totally wrong! Perhaps they can all be found with a sufficient adversarial loops or something. I just have a really hard time imagining no problems of this sort occuring.

*(Memory leaks can probably be found by just having the LLM run valgrind itself and chase them down, but this gives you a good feel for the difficulties of writing safe C. Again, never tried any of this with LLMs myself, and I haven't written a nontrivial C program in years.)

Do you really think current LLMs can implement a large application in C as securely as they can in e.g. Go? I will freely admit that I have not tried to do so but I have a hard time imagining it. Perhaps my biases are outdated...

Changing {} to [] seems like a very strange suggestion to me. {} is used here because it's the way you group things in LaTeX. If you were going to change it for human use, why not just use parenthesis? What's wrong with {} in the first place?

There is money in this, so of course the closed models are far ahead. The open models will likely catch up a bit at some point, just as Stockfish caught up to AlphaZero. That being said, there are already a couple. It seems Deepseek has a claimed proof to the "Ziegler's Cross-Polytope Conjecture" [0], but I can't speak to the significance of the result.

[0] https://arxiv.org/abs/2606.31640

There is no evidence that I can find for the claim "a bug in the Lean kernel was discovered last week by way of an LLM tricking itself and its handler into believing it had found a non-constructive proof of the existence of a nontrivial Collatz cycle."

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!

If accomplishments can't be distinguished between talented people and untalented people with compute, is there really a point in trying? I suppose one can hope that talented people given compute will be more effective than untalented people with compute, but I despair that that may not be true for much longer.

Presumably it's a rounding error compared to their full output, and they're making sure they have enough compute set aside for research by limiting public models. The more datacenters they build the less they have to limit them.