They're solving them in a way that isn't particularly interesting because it's near impossible to read and understand, and follow, what the LLM did. It's this way not because it's so smart, but because it's so stupid and still reached the goal by pure force and effort.

I am sorry but your argument looks to contradict itself: They solve hard mathematical problems because they are stupid and use brute force? Then why a human skilled in mathematics guided them for many turns in their conversation?

If they were really stupid, say like a Prolog program or a solver, only stating the goal was enough,

Can't you kind of think of them as a genetic algorithm that has a very good hypothesis generator? Humans could, in principle, help guide that (already very impressive) hypothesis generator to make better guesses to find the proof more easily.

[delayed]

Conversations with an ChatGPT with Terence Tao at the helm are a thing of beauty. An advanced practitioner prompting things beyond my understanding. Jarred Sumner's paper on the Riemann Hypothesis, however, was not that. No slight against him, but Jarred was a non-mathematician, and his prompting to improve the minimum fraction of zeta zeros by Claude amounted to "keep going" and "believe in yourself". Shit, anyone coulda done that in his position.

https://www.anthropic.com/research/riemann-zeta

My point is that it does matter who's driving the AI but it also matters the route. Just like F1 champion Max Verstappen is a ridiculously better driver than me at driving an F1 car around a track, if we're just driving a friend to the airport, it doesn't really matter if it's Max or me driving, so long as we don't crash.

I don't know how to communicate this, but what you are saying is almost entirely wrong.

People can follow what they did. The documents OpenAi produced in their big drop are hard to read because they are poorly written in weird ways, not because they are beyond human intelligence. They didn't brute force in the normal sense. AI doesn't get tired, so it can try 1000 promising ideas, but it's like 1000 Ph.D.-level mathematicians trying different ideas, not 1000 calculators trying all combinations.

The biggest results -- quasi-Riemann, no Siegel zeros, and Unique Games Conjecture -- have already been digested by experts. No Siegel zeros in particular already has like five different write-ups, and Tao has written a exposition on his blog.

So did we get any new mathematics out of this, or just solutions to problems without new techniques or insights? I haven’t been able to keep up with this or read the writeups you mention, genuinely wondering since this seems to be a central concern of the math community

It's only been a month and people aren't that fast, but I think yes. Analytic number theory and complexity theory were stuck on the lack of progress on certain questions, that is now unstuck.

A relentless low IQ person with broad knowledge and no need to sleep, I guess?

[delayed]

You mean techniques like using the prompt of mathematicians in the training set and brute force a solution before they publish?

[delayed]

I'm more interested in the techniques used to generate these proofs, and how they can be improved to be as reliable at solving a broader class of problem than already formalized mathematical conjectures.

I think it does gel. You're right that the comment you're replying to is weakened by that fact.

It gels because they solved about 700 problems out of 4000 attempts. And they threw a ton of resources at each. So "per problem" it's less than 1 in 5, "per token" it's probably not a great record. I mean it's astonishing that it's possible at all of course. But on average, even an expert with a top model will probably have an underwhelming response to the vast majority of prompts.

and I'm guessing it was with "tool calling" ie. they can write a bunch of Lean proofs and hit compile and basically brute-force a whole bunch of hypotheses quickly?

Ie. the LLM itself isn't as "smart" as the combination of LLM, Lean, looping, search and vast gpu/cpu-time.

In my experience they write an informal proof first, check it without Lean, and only then turn it into Lean code. What they're truly bad at is explaining their proofs. Until they improve at that, we'll have to keep asking Lean whether they solved something correctly.

While they're not great at explaining their own proofs, some models are good at explaining older, human-written proofs.

I definitely don't know but I got the impression it's the opposite. Based on the observations about Navier Stokes and the natural language proof not matching up with the lean proof and other things. They generate lean and convert it into natural language at the end. But really I could be wrong just giving anyone interested a lead to check out.

You cannot brute force lean proofs of any complexity. The space is infinitely large.