> A good sign that LLMs have reached human level for a much wider class of problems will be if they start proving theorems using methods that, like much of the very best human mathematics, are new and surprising but that with hindsight come to seem beautiful and natural. They should also be methods that are difficult to stumble on by accident. It is hard to say precisely what would count as such a proof, but I think we’ll recognise it when we see it

Agreed. I find that after seeing these results from OpenAI we undeniably have a machine that has:

* General knowledge of nearly every subject humanity has ever learned

* The ability to simulate reasoning (albeit sometimes not very well) with that knowledge

* The ability to reference across the domains of knowledge

To me, this is more or less what I would think "Artificial General Intelligence" is. It's the cumulative knowledge of all general human intelligence, baked into an artificial form, which can then use that knowledge to achieve novel goals.

In many cases of mathematical breakthroughs there is an insight that comes from just happening to know a combination of already existing ideas and then combining them to solve that problem. This is where having that general knowledge seems particularly strong because we can run these machines for weeks on end effectively trying to brute force.

That being said, I could never imagine an LLM in its current form inventing something as elegant as the Fourier transform.

>> To me, this is more or less what I would think "Artificial General Intelligence" is

So then you need to explain ARC-AGI-3: https://arxiv.org/abs/2603.24621

"Our testing shows humans can solve 100% of the environments, in contrast to frontier AI systems which, as of March 2026, score below 1%."

Back 1996, EQP automatically solved the Robbins conjecture. But nobody concluded EQP was generally intelligent.

https://www.cs.unm.edu/~mccune/papers/robbins/

Would you trust a bridge built by it with zero human interference? A train? A plane? A skyscraper? What about fight in a war? Unless you can, I wouldn't consider it AGI, because you're actually trusting human intelligence to verify the bridge or train or plane or skyscraper is safe or that the robot is following orders. And even then, you're trusting human-influenced guardrails etc. I would consider it AGI when an AI-created LLM can do all of these things and you trust them with your children's lives. Would you trust an AGI cop to protect your children from a violent criminal? Unless you can, believing what we have as AGI is just an empty opinion with no meaning behind it.

I would be extremely surprised if something as elegant, terse, and useful as the Fourier Transform had been missed by human mathematicians up until now. All expressible theorems are enumerable, after all (if we limit ourselves to a finite alphabet). It seems likely that any new theorems are long, highly complex and esoteric, regardless of human or machine origin.

That’s not the criteria outlined in the quote you just used.

IME, LLMs are primarily good at grinding through cases, which is why you see them pushing upper and lower bounds and finding counter examples.

I spent a few weeks working on a number theory proof with Claude off and on and it spent hours and hours and hours grinding through one shape of polynomial after another, reporting "progress", and it's true, it proved what I was trying to prove for more and more classes of polynomials, but it was biting off pieces of an infinite tower of classes with no hope of closing it for _all_ polynomials.

That happens to be a good way to find counter-examples, though, and when I posed a slightly different version of my problem, it found a counter example in about 90 minutes.

And in fact, finding the counter example for the related problem allowed Claude to finally prove the thing I wanted to prove to begin with, by lifting the problem to a characteristic where that counter example didn't exist, proving my question there, and then proving that it still was equivalent to my original question.

I share the same thinking. What do you think is a good way to try to define this "elegance"? If we try to use the mental framework of

Step 1. LLM "brute forces" a search

Step 2. We train on this trace

Step 3. In the next model, LLM internally makes a "shortcut" for this path and "brute forces" it quicker (or one shots its in the best case)

And we want to ultimately show why that definitio evades this framework.