Two days ago OpenAI published ten new results in mathematics and theoretical computer science, all found by an internal version of Astra, their next model.
The list has sphere packing, non-sofic groups, circuit lower bounds, quantum games, the closest vector problem, and five other things I understand even less. I know enough theoretical CS to see a few familiar words and not enough to tell you if the proofs are actually beautiful.
So yea, I asked a model to explain what the model had done.
The successful runs used enough tokens to cost around $2,000 at Sol API prices. Humans, with help from the same model, prepared the arguments into a 249-page paper. Astra then formalized them in Lean, and OpenAI released the certificates on GitHub.
Model finds proof. Humans make paper. Model makes sure proof compiles.
Kinda rough place to be standing in that pipeline lol.
The day after, Fernando Borretti wrote Mathematics Without Mathematicians. His point is that people keep finding one last important job for the human. We will pick the problems. We will explain the answers. We will decide what is worth keeping. At the very least, somebody has to understand it all.
Then the models get better and that job disappears too.
I wanted to disagree with this. It would be nice if he was just doomerposting and we could all go back to whatever we were doing. But “humans will have better taste forever” is not a bet I feel great about making right now. Neither is “the models can prove it but surely they cannot explain it.” Every permanent line people draw around us has started looking suspiciously temporary.
What actually bothered me was the Lean part.
The $2,000 makes discovery cheap, but Lean makes the result checkable without trusting the model’s prose or waiting for a person to understand 249 pages. Another model can take the checked result, use it somewhere else, and pass that result further down. Math to science to engineering, and somewhere at the end we get something that works.
The proof never has to fit inside one person’s head.
I know the small version of this from code. I can send an agent into a project I know nothing about and get back a working diff. The tests pass, the feature works, very cool. Then I close the terminal and realize I could not rebuild the same thing on my own.
Sometimes I learned something. Sometimes the task just got completed near me. Both look exactly the same in git.
That is the bit I cannot stop thinking about. Not whether the output is real. The output is real. It is whether anything happened to me while it was being made. Like, did I spend a single brain cell in the process?
And now I am supposed to go learn some of the subjects in that list. Spend a few years getting through the basics while the frontier is apparently doing this.
Amazing timing bro.
If learning was only a long route toward becoming a useful answer-producing machine, then we may be cooked. There is no honest motivational quote I can put here that fixes that.
But then I look at the stuff I already make. X already had a website before I built Xeet. Torrent clients existed before tork. macOS had a settings app before I rebuilt the same machine 254 times with Nix. None of these projects began because humanity was stuck waiting for me to save it. Nor did I make the world a better place or whatever. I saw something, got annoyed, wanted to feel cool, or was just curious enough to see if I could make it work differently.
Having a better tool already available did not kill that feeling.
Maybe math can still be like that. Not “the humans remain economically necessary” or some other cope with a six-month expiry date. Just that knowing a thing and receiving the answer to it are different experiences. A model can give me a perfect explanation, but it cannot do the understanding for me. That part still has to happen in my head.
This does not save mathematical jobs, status, or the whole social world around research. Borretti is probably right that very few people can run on pure intrinsic motivation forever. I definitely cannot predict what any of this looks like in ten years.
I also do not need a ten-year philosophy before opening a book today.
Astra can reach the frontier before I understand the problem statement. Fine. I still want to know why the thing is true.
Maybe that is cope too. idk, ask me again after I figure out what a non-sofic group is.
