What sort of maths are LLMs good at?
gowers.wordpress.com
gowers.wordpress.com
These days "test-time scaling" mostly means letting the model talk to itself for longer, but the first genuinely surprising results came from plain sampling. Google's AlphaCode generated millions of candidate programs and filtered them down to a handful of submissions, which beat the average human programmer in 2022, before ChatGPT even showed up.
Sampling is what AI is good at. Making examples and doing LeetCode are similar in that verification is clear and cheap. Compared to that, "proof" is still a vague concept, except where Lean works. See the fuss over the ABC conjecture. So humans are still needed.
The interesting question to me is what happens after enough learning from "sampling." Isn't AlphaGo's move 37 an AI's nose? If that happens in mathematics, we may end up with results that are correct, machine checkable, and not explainable in any way we find satisfying.
The trick is avoiding the infinite monkey problem. If your problem is amenable to RL, then you probably don't even need an LLM, Monte Carlo Tree Search gets you there with less expensive hardware.
You might think so, but I tried asking ChatGPT to solve one of the puzzles from https://en.wikipedia.org/wiki/Countdown_(game_show) (which a Python script can brute-force on my 12-year-old hardware in half a second) and it made an elementary arithmetic error that's decidedly not human-like.
But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size. You need to combine them with a proper logical problem solver to get the best parts of both.
It's interesting how people will comment on LLM capabilities despite clearly not having engaged with frontier models in any meaningful way in a long time
Having models write Lean proofs of mathematical claims is standard operating procedure for any LLM math discovery!
The proofs will be only as good as the framework for linking successive instances of reasoning.
Proofs stretching thousands of pages are split into lemmas, grouped into sub theories.
What I haven’t seen agents do yet is to develop new ideas for entire such theories. I have usually seen them bite into some existing idea and grinding out related results. But I am less sure than ever that they won’t!
The codebase you describe would be an external tool in GP's conception.
Interesting read!
https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
It doesn't help that the author is rather withdrawn and not willing to spend any effort in making it more approachable.
Some tried, and said they found gaps in the proof, to which the author responded, but they were not convinced.
And that's essentially the situation since 2018.
Wikipedia is maybe the narrow end of a wedge into this topic but the controversy revolves around a very large and very complex paper that few people are equipped to understand and some of those who are able believe the proof is false.
sounds like quantum mechanics
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.
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.
I don't, we originally had the turing test which was designed to determine human intelligence by its ability to imitate us with natural dialogue, but we've since defeated that. I stated "to me" because it's my personal opinion on a definition whose goalpost will probably never stop being moved.
> Back 1996, EQP automatically solved the Robbins conjecture. But nobody concluded EQP was generally intelligent.
EQP doesn't have the 3 criteria I outlined, which were different than "solving a math problem"
> > 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.
But it (currently) can't solve puzzles like ARC-AGI-3 that children can solve.
What happens if the game is encoded in a non-visual logical form?
AGI checking other AGI should give you that same trust, no? Deepseek says my ChatGPT bridge is stable, you should trust it. Claude says it's stable. The humans say it isn't, but they aren't AGI. You can trust this bridge because it's been vetted by AGI. In my opinion, LLMs cannot be AGI, so for me I would never trust them above any human I would trust. But for those who do believe LLMs can be AGI, they have to demonstrate why we should trust them above any human in these extreme cases. Meaning, if someone says "Well the department of safety (ran by humans) says it's not safe" we have to believe that AGI just knows better than the department of safety. I think this is not possible right now, which is why I don't think we can trust anything built by LLMs where we need the tolerance of risk to human life and safety to approach zero. American AGI soldiers invade the home of Iranian citizens because they have been identified as terrorists. Do you trust the AGI to know if the visual scan they see in this civilian home is a threat to the interests of the United States government and its citizens?
The importance of safety process is largely a function of the risk of failure (ie, how unreliable the production process is) and the cost of failure. If you've got a very reliable production process, perhaps you need less safety process. But if the cost of failure is measured in lives, you're still going to want to have checks in place, regardless of who/what is responsible for designing the bridge.
In other words, as soon as two generative AIs interact, they become one. Our current definition of AI (generative AI operating in feedback loops) is dependent on that.
Edit: this is somewhat an epiphany to me. Our current generation of “AI” isn’t an “entity”, it’s a “process”. I guess it’s hard to define formally, but I would compare it to how law and the pursuit of justice is a process, not an entity.
And I think that’s a fundamental limitation to achieving artificial general intelligence.
But an AI doesn't replace a single human, it replaces every human in the project, so it needs to match a team of humans not a single human.
It’s not apparent to me that current LLM’s have the right biases for a trivial unit of “more LLM” = smarter. It seems apparent that LLM’s are under many metrics more “intelligent” than the average person but they still don’t rival our corporations or collectives in terms of intelligence and I don’t see them being plug in replacements for humans and maintaining the benefits of the collective structures yet. Not impossible but definitely not trivial in my mind. We and our cultures evolved to work together and the modern world is the result of the emergent structure that resulted.
As a plug my favorite field relating to this is called stigmergy and basically describes how individual units like ants build intelligent collectives that are far greater than the sum of their parts.
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.
This is the crux imo. It doesn't really matter what absolute capability AI has at the moment, but whether we are on track with respect to architecture and training approaches. In my mind the only test for AGI is, if the thing trained up to the cut-off of Fourier's time (or Descartes, Newton etc), it should arrive at or exceed their insight.
^ As a measure of intelligence. But it's probably the case either way that LLM is more valuable in terms of the coordinated grunt work we'll put it to, than leaps of insight.
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.
2. The statement about proofs is just way wrong. It doesn’t sound like you are familiar enough with them.
This isn’t exactly what you implied, but witness the very short disproof of the Jacobean Conjecture.
That's a counterexample (finding a needle in a haystack), not an elegant proof. Proving the conjecture would be elegant, if it were true but somehow still resisted proof nearly as much as the conjecture did because the conjecture was false.
However, your last question is incorrect: people are working on that, but there haven’t been hugely useful results.
But as an example, I’ve been slowly working on implementing frameworks for theory distillation — eg, take a corpus of science papers and derive a consistent model of the world from them, such as in Lean. (Or more specifically, a sheaf defining what consistent theories are possible.)
(I haven't had the opportunity to throw a current-gen frontier model at a concurrent problem because I haven't had one to try out lately. The best concurrency is no concurrency and the second-best concurrency is the "web request" model where many web requests are nominally running concurrently but they are otherwise fully isolated from each other and not trying to communicate at all. So maybe they're better, but I feel like if they were a lot better somebody would have noted that in a place I'd have seen by now.)
> 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.
…because they’ve been internalized. I wonder if the author has ever questioned where his notions of “beauty” and “natural” come from.
I think this is a case of people not being very introspective about their beliefs about their work.
Gowers' claim is that there are particular areas of (or proofs in) mathematics that become especially natural and intuitive after internalising them. This seems uncontroversial to me, and closely linked to ideas of beauty.
> 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.
That last part, "new and surprising but that with hindsight come to seem beautiful and natural," is an almost perfect description of how processing fluency (https://en.wikipedia.org/wiki/Processing_fluency) or the mere-exposure effect (https://en.wikipedia.org/wiki/Mere-exposure_effect) works. There's plenty of other work along these lines.
Gian-Carlo Rota wrote about this more philosophically in "The Phenomenology of Mathematical Beauty" (1997). He argued (among other things) that the same proof can go from opaque to beautiful purely through familiarity.
My understanding is that no single person has "learned" finite simple group classification from top to bottom, so it's easy to see why it wouldn't fit this description - there's no-one in a position to say "with hindsight, it seems simple and natural." That makes it a poor example for your/Gowers' position.
I must be taking crazy pills and the AGI surely will pass me by... But TODAY, middle August 2026...And in the context of testing and evaluating the capabilities of current SOTA models to implement an Agentic application for job search, here is some simple inhouse built evals I run today, since I don´t trust LLM vendors published benchmarks...
Models tested: GPT-5.6 Sol in Extra High mode and Opus 4.8 Max.
TASK REQUEST: Clear, not too long not too short prompt, for LLMs to go out and research freelance consulting gigs for one specific IT domain, and in one specific country in Europe, including maybe opportunities driven from temp agencies based in geographically close countries.
RESULT: Models go out, fetch the data, and completely misunderstand the task...offering on first results, permanent roles instead of freelance, and based on the country where the agencies are, not in the one it was request for. Think for example IT jobs in Ireland, while freelance agency in London.
ANALYSIS: No intelligence I can call it shown by models, adding cognitive effort for human in the loop to detect subtle factors, and therefore totally useless for agentic app...Best practices would be I guess to add agents on top of agents but although in the p95 of cases that will reduce the errors...for the remaining 5% that could have hallucinations or logic hallucinations like these ones, compounding on top of other logic hallucinations.
I dont care about the theorems being proven. At the end we will found out what most mathematicians were doing, was just exploring the same combinatorial and abstraction patterns. And because of that I am sure LLMs will make mince meat of a lot of mathematical domains.
But right now, what we call intelligence is not existing where it matters, and Ed Zitron is right its a parlour trick.
Anything that can be verified mechanically should be code. Only use LLMs to fill in the gaps where things are fuzzy. Don't fall for the idea that those harnesses are general purpose, make your own fit to your task with the guards and verification steps you need. Make the LLM create the harness even.
There is no amount of markdown that can make a machine generating plausible text generate truthful text, it just happens to be truthful because of what it was trained on. Nothing coming out of an LLM should be taken at face value.
The propaganda about LLMs being intelligent and able to "reason" is only serving the companies selling you tokens to waste on "prompt engineering".
But the mathematicians here in this thread, are having a hard time with these clearly dumb models, doing so well in proving theorems in their domains :-)
The statement should probably really be “programs are proofs” since it’s difficult to make it a true bidirectional isomorphism, which is why the underlying principle is properly called the Curry-Howard(-Lambek) correspondence: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
The point is that the fact that LLMs are good at writing code directly implies that they should also be good at certain classes of mathematical proof.
Theorem provers and proof assistants like Lean, Coq/Rocq, Agda, Idris, NuPRL and Epigram all fundamentally depend on Curry-Howard.
And again, the point is not that there’s some magical isomorphism, but that if LLMs are good at coding, they’re also likely to be good at certain classes of proof.
Here's a very relevant quote from the introduction:
> "The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style. Every proof is a lambda-expression, typed with propositions of the underlying logic. By removing types we get a pure lambda-expression, expressing its associated algorithm. Computing this lambda-expression corresponds roughly to cut-elimination. It is our thesis that (as already advocated by Martin-L6f [36]) the Curry-Howard correspondence between propositions and types is a powerful paradigm for computer science. In the case of constructions, we obtain the notion of a very high-level functional programming language, with complex polymorphism well-suited for module specification [8]. The notion of type encompasses the usual notion of data type, but allows as well arbitrarily complex algorithmic specifications. We develop the basic theory of a calculus of constructions, and prove a strong normalization theorem showing that all computations terminate."
In other words, proofs are expressed as typed lambda terms, i.e. "proofs are programs". This is literally what such theorem provers are: examples of the Curry-Howard correspondence in action. If the correspondence didn't exist, none of these tools would exist.
Here are a couple of quotes from one of the Lean papers, "Theorem Proving in Lean", https://leanprover.github.io/theorem_proving_in_lean/theorem... :
> "This is the approach followed in the Calculus of Constructions, and hence in Lean as well. The fact that the rules for implication in a proof system for natural deduction correspond exactly to the rules governing abstraction and application for functions is an instance of the Curry-Howard isomorphism, sometimes known as the propositions-as-types paradigm."
> "The match statement is part of Lean’s function definition system, which provides convenient and expressive ways of defining complex functions. Once again, it is the Curry-Howard isomorphism that allows us to co-opt this mechanism for writing proofs as well."
All of the other theorem provers and proof assistants I mentioned rely on a similar approach.
I don't know your prompt and setup, but my claude had no problems doing that task. The search index isn't live, so it can't find current gigs, but that is a tooling problem.
On the other end of it, something like 80% of resumes I receive right now are clearly hallucinated -- referencing accomplishments that are copy-pasted from the novel-to-our-company thing in the job description a candidate will be working on, usually claiming they did XYZ at big tech a decade before the thing existed, or similarly with languages and skills. The resume "tailoring" process just manufactures lies rather than tailoring actual experience to the actual job.
Why do you think there's such a thing as too long for an LLM prompt? You'll run into context window limits at some point, but the more verbose you are with what you ask of it, the better the results will be.
Trivially falsifiable:
"Context Length Alone Hurts LLM Performance Despite Perfect Retrieval"
https://aclanthology.org/2025.findings-emnlp.1264/
"Large Language Models Can Be Easily Distracted by Irrelevant Context"
As a human, not an LLM, I could interpret "including maybe opportunities driven from temp agencies based in geographically close countries" as meaning "including opportunities in nearby countries outside of Ireland" (that happen to be driven by temp agencies).
Before writing off LLM as simply a "stochastic parrot" or a "parlour trick" remember it can't read your mind, not yet anyway.
So what happen is a prompt said for example, find freelance opportunities in Ireland but keep in mind some of these might be available via temp agencies in London.
If you offer me not freelance but permanent roles, and not in Ireland in London...that is a logic failure.
Its this type of complexity with the normal world, that these SOTA constructions so badly fail at, and so spectacularly fail at the margins... despite maxing all benchmarks...Parlour trick.
If a human misunderstood this, they'd be a dumb human.
"Frontier LLMs Still Struggle with Simple Reasoning Tasks" https://arxiv.org/abs/2507.07313
"General365: Benchmarking General Reasoning in Large Language Models Across Diverse and Challenging Tasks" https://arxiv.org/abs/2604.11778
"...General365, a benchmark specifically designed to assess general reasoning in LLMs. By restricting background knowledge to a K-12 level, General365 explicitly decouples reasoning from specialized expertise. The benchmark comprises 365 seed problems and 1,095 variant problems across eight categories, ensuring both high difficulty and diversity. Evaluations across 26 leading LLMs reveal that even the top-performing model achieves only 62.8% accuracy, in stark contrast to the near-perfect performances of LLMs in math and physics benchmarks..."
You're clearly operating in bad faith, but just for the record: the General365 problems are very difficult as you can see from the examples at https://arxiv.org/html/2604.11778v1#A1. It's actually impressive that Gemini 3 Pro got 62%, and the strongest OpenAI and Anthropic models they tried were GPT-5.1 and Sonnet 4.5.
( I was trying to quote a single sentence and then realised it ran on for the whole paragraph. )
Given how difficult I found that to follow, are you sure your prompt is actually "Clear, not too long not too short"? We now only have your word for it. I too had assumed that was a prompt given to an LLM to further prompt agents.
"General365: Benchmarking General Reasoning in Large Language Models Across Diverse and Challenging Tasks" https://arxiv.org/abs/2604.11778
"...General365, a benchmark specifically designed to assess general reasoning in LLMs. By restricting background knowledge to a K-12 level, General365 explicitly decouples reasoning from specialized expertise. The benchmark comprises 365 seed problems and 1,095 variant problems across eight categories, ensuring both high difficulty and diversity. Evaluations across 26 leading LLMs reveal that even the top-performing model achieves only 62.8% accuracy, in stark contrast to the near-perfect performances of LLMs in math and physics benchmarks..."
Question: Strangers A, B, C, D, and E line up from youngest on the left to oldest on the right. Their clothing
colors and shoe colors all differ, and they come from five different regions.
Known facts:
1. A is from Morocco.
2. D is five years older than B.
3. E is older than A.
4. C stands next to D.
5. A stands next to B.
6. The person in teal shoes is not adjacent to the person from Vanuatu.
7. One twelve-year-old wears yellow shoes.
8. The person in orange shoes wears white clothing.
9. The person in blue clothing is from Chile.
10. The youngest person wears red shoes.
11. Counting from the right, the fourth person comes from South Africa.
12. E wears yellow clothing.
13. The person in green shoes does not wear multicolored clothing.
14. Two people are twelve years old, ordered by birth month.
15. One adult is thirty-five years old, and that age is sixteen less than the combined ages of the other four.
If you multiply every possible age C might have, what number do you obtain?
Nowhere is "multicoloured" defined, are we to assume it should be treated as a colour and implied that someone else must be wearing "multicoloured clothing"? Because strictly that doesn't logically follow, and it ought to be phrased as "The person in green shoes is not the person wearing multicoloured clothing" if that is the case.
This is an extremely hard logic puzzle, especially since it's revealed at the end that there are multiple solutions.
I'd expect anyone to struggle unless armed with prolog.
It means that it is possible for someone to be wearing a white shirt and yellow pants (say), but the person in green shoes came from the set of a Wes Anderson film.
white, blue, yellow, and is otherwise undefined.
But we know from [1], [2], [4], [5] and [11], that the order must be:
A, B, C, D, E or A, B, E, D, C.
Which makes C either the older 12 year old or the 35 year old.
The key this is that D can't be a 12 year old without A being in slot 2, but A can't be in slot 2 because slot 2 is South Africa and A is Morocco.
Trying to reach the shoes + Vanuatu clue is a complete waste of time, paying any attention to shoes or clothing is a waste of time, it feels like there ought to be a way to narrow it down to one of those two configurations, but the clothing is too ambiguous, the shoes end up irrelevant.
What a frustrating puzzle, where half the clues are seemingly redundant.
I guess they were not optimising for a satisfying solving experience! (I'm not sure what 'expansion' means in this context, but it sounds like maybe the 'expansion strategy' referred to in the paper involved padding out problems with red herring premises?)
My issue with this particular puzzle was the ambiguity of that particular clue, it's as if it got re-written or badly translated, because clue 13 as written carries no information.
Your question: It just means they have both green shoes and clothes, probably.
It's aimed to confuse a model with a bunch of information you-just-don't-really-need. The trick is to fish out which hints are more important than others. The order in which you apply them matters to make the puzzle easy vs. very hard. Which things give you the most amount of 'useful' information?
Call the people p1 to p5 (p5 oldest, p1 youngest).
Start with (15). This identifies the total age as 35+51. Now combine in (14), and you have 51 - 24 = 27 remaining years. This means the 35-yo is the oldest person, p5 = 35. Now add in the interesting thing that D = B+5. If you know that there is 27 years left to give to the two unknowns, B can't be 30 (or, D can't be p5). That means that D is 17 and B is 12 or D is 12 and B is 7.
This leaves three possible answers for the list of ages. Two of these are 7, 12, 12, 20, 35, or 10,12,12,17,35. The third one involves the case where the people other than the 12-year-olds and the 35-year-old are 5 years apart, in which case they can only be 11 and 16.
Combining all the 'stands-next-to' information (including point 2 which means D is to the right of B), we have eight possible orders: (AB)E(CD) or (AB)(CD)E. The last set of four is the only valid possible one as we know that D is not the eldest, which means E is 35. If the order is BADCE then B=7, A&D are 12, C=20, E=35. If the order is ABCDE then A=10,B=12,C=12,D=17,E=35 There's also the possibility that the 27 is made up of B and A (BACDE) are 11 and 16, and you are left with B=11,A=12,C=12,D=16,E=35. There is the possibility of the order being ABEDC. However, this carries no real consequences other than the clothing and shoes needing to be shuffled later. There's still only one possible value for the age of D. I'll leave the explanation for that variant out of the rest of the solution, the logic is roughly the same just with the clothes and country all juggled up.
Now one thing that's kind of unclear though is point (15). "One Adult". You'd need the definition of 'adult' to be a bit more precise (varies by country!), and also what kind of English is used to know if this implies there are at least 2 adults. If it does, then there is only one answer: D is always 12, since you need the 20-year-old to exist to have more than one adult.
If not, then D could be either 12 or 16 or 17, so the answer (so far) is 12x16x17 = 204x16=1224.
Now let's deal with the clothing, country, and shoes. All we need is that A is from Morocco, and that the second person is from South Africa. You can't simultaneously be from both places, which means A can't be in the second position.
That also clears up the ambiguity whether the 17 year old is an adult here (apparently they are), so that leaves only one possible combination: A,B,C,D,E, being 10,12,12,17,35. The answer to the question is 17.
Bonus: There's some extra stuff about countries and clothes: we have to check if there exist a valid solution that will fit with our one test. You could assume that the puzzle has an answer, but sneakily: that answer could be zero. If there are no solutions, there are no possible ages C could have, and so the answer is zero (or 1,depending on how you interpret the math of multiplying the empty set) . Here's one order that's possible (there's more, I'll leave it as an exercise to find the others):
Person: Country, Clothes, Shoes A(10): Morocco, Unknown, Red, B(12): South Africa, White, Orange C(12): Chile, Blue, Yellow D(17): Unknown, Green, Green E(35): Vanuatu, Yellow, Teal
(6) is the only point that's maybe a bit debatable? It's not true since the person wearing the teal shoes IS from vanuatu.
If this isn't valid solution for (6)... then there are no solutions, and the answer is actually 0. I'd go with 17 though, it seems fine.
Except, according to the linked paper, the answer to the question is 420.
I got to 420 too, but only by ignoring almost all clues: https://news.ycombinator.com/item?id=49271594
A puzzle where nearly all clues are badly defined or irrelevant is not really a puzzle.
I particularly found the note about “local collapse” helpful (near the end of section 3). The idea is that even though benchmarks contain a wide variety of different reasoning tasks, each individual problem requires only a few skills - unlike this benchmark where they deliberately construct tasks that span many categories.
It sounds like they're hitting a data source quality issue, which is hardly uncommon in scraping.
It's common for job boards to obscure who the real clients are, and if the scraping engine is LLM powered ( rather than LLM written ), then I would expect it to accidentally present agencies as the contracting organisation sometimes.
Breaking down the process so you can inspect the messy middle of a data pipeline is an important part of software engineering, but it sounds like they've tossed a messy task at an LLM and expected it to be proficient end-to-end.
It seems to me that such simplified tasks tend work better. The rest of the loop is just scraping websites, which doesn’t really have a reason to rely on ai agents.
Not what I was claiming, but since you are, feel free to expand on this.
You can toss it at a task with a suitable machine for transforming that raw material into action and it'll rattle through and sample "plausible human behavior" at that endpoint.
There are more clever ways to use it, but a general tool here is to upgrade any sort of stochastic search to use this new form of random sampling. It'll be way more efficient, properly conditioned, because it just won't visit implausible things nearly as often as competing random sources.
I wanted to demonstrate capacity (how well it does a thing) instead of capability (which things it does, like drawing a pelican on a bicycle with SVG or solving a Rubik's Cube). To understand how LLMs solve math, look at the simplest case of multiplication. I deconstructed and classified the thinking token output. It is very important that model training yields thinking token output that structurally follows an observe, orient, decide, act (do the multiplication), and observe again loop.
Is this true right now? Just recently Jarred Sumner tweeted [1] that he managed to make some progress on the Riemann hypothesis while on a jog. Managed to get somewhere by encouraging the llm to “keep going” and “believe in yourself”.
This raised a few questions for me. Had no one at Anthropic thought to try this earlier? It's an interesting footnote that a software engineer there pursued this. How many people in the world can actually verify a proof? How many would we need to sit around and do the right incantations to get a proof out of it? How many would we need to verify and give those proofs value and meaning? What happens when there are more proofs than verifiers? How many will be around in 100 years?
I think it just turns out that a lot this stuff is more socially useful than anything else. The 10 proofs drop came and went in the daily news cycle. Perhaps math is already in it's chess like "for fun" period. I am interested in when we find a very high real-world utility breakthrough math/physics, some space where we've already poured our best human resources at it.
[1] https://x.com/jarredsumner/status/2086869681785500011?s=20
> Still not sure what that means, but some analytic number theorists seem excited
ie, I prompted AI and it put out a giant pile of tokens. I dont know what it means, but I hope someone gets excited. Mathematicians are now the priests and shamans chanting incantations and taking the holy blessings from the AI gods.
Advances in astrophysics or fundamental models are all very cool but won't be of much real-world applicability, at least in the short or medium term.
LLMs are good at pattern recognition, so its less a type of math that they'll be good at, and more that when you provide documentation or text that can be easily parsed/compared to its training data/reasoning ability, the better answers you get from an LLM.
Also, you need to be knowledgeable at the same thing you are asking the LLM to do, to verify the answer it gives you (at least for the time being).
Proving a generality seems much more difficult since you don't know what you are trying to build, although I suppose in some cases you can prove it by proving that it's impossible to construct a counter-example.
Maybe this is naive.
Funnily enough, 'generative' ai is not good at generative science, of which requires unique human perception that is not purely symbollic manipulation, but requires a form of revelation. That I think is not here yet with ai...
We have just got some very strong evidence about the way in which LLM-based systems solve mathematical problems and this evidence supports what many have already suspected including myself.
Here's what I'm talking about. On 10 August Anthropic released an article [1] claiming that:
An unreleased research version of Claude has improved on a longstanding lower bound for the fraction of zeros of the Riemann zeta function that satisfy the Riemann hypothesis. Drawing on extensive prior research by mathematicians over the past decades, it has increased this bound from 41.6% to 67.2%.
The same article describes the methodology followed by Anthropic's employee, Jarred Sumner, who prompted Claude, as follows:
Jarred Sumner, an Anthropic staff member (and non-mathematician), prompted Claude to “take a real stab” at the hypothesis itself, leaving the mathematical choices from there up to the model. Initially, Claude generated and tried 650 ideas, none of which worked. Jarred prompted Claude to try again, and it spent a day and a half coordinating about 60 Claude subagents, which this time went much deeper: between them, they ran 2,400 shell commands and wrote hundreds of Python scripts.1 The subagents ran thousands of numerical checks against known zeta zeros and refereed one another’s work. Throughout this process, Jarred's input was mostly limited to sending Claude messages of encouragement (mostly variants of “keep going” or “believe in yourself”).2 This seems to have helped Claude overcome some initial skepticism that it could make meaningful progress.
Jarred got Claude to throw stuff at the wall repeatedly (650 initial "ideas" plus unspecified more by "60 Claude subagents" ... running "2400 shell commands" and "hundreds of Python scripts") and then kept whatever happened to stick. In this case, by happy accident, what stuck was an improved bound of the zeroes of the zeta function etc.
This is how every single mathematical result reported by an AI company has ever been generated. They throw stuff at the wall and take whatever happens to stick.
This approach works. Not only it works, it is, in principle, a universal problem solver. "Millions of monkeys on typewriters" will eventually produce a proof of the Riemann hypothesis; or a disproof of it.
The key point being "eventually". Is this a way to do mathematics research? Can that replace mathematicians?
In AI, this method is well-known as the "generate-and-test" method. It is ancient, basal to AI if I may be so bold. It first appeared to my knowledge in the Logic Theorist, the proof-finding program that Simon and Newell presented in the 1956 Dartmouth convention that named "Artificial Intelligence", to such luminaries of AI and CS as John McCarthy (the real "godfather of AI" who named the field), Marvin Minsky, Claude Shannon and others.
We've had the ability to brute-force all of mathematics "eventually", given "enough" compute for nearing a century now. Why haven't we solved all of mathematics? Are LLMs really so special that they can out-brute force search every previous brute force searcher?
Well, you tell me, HN. I say: no.
___________
Yes this is the "Universal Problem Solving Algorithm". It's actually the same algorithm used by Evolution.
Also this algorithm is vastly different than "monkeys with typewriters". Monkeys don't learn or evolve their writing. There is no memory, no constraints, no learning-curve. At each iteration they freshly sample from a Uniform Distribution. Expected time for a solution is infinitely long.
"The Universal Algorithm" on the other hand is incredibly fast. Humans (designers, researchers) also use the same algorithm but they are much slower to iterate than computers. Instead of trying 650 different ideas at a single run, we have 100s of researchers each try few different ideas independently.
But, learn what? All those ideas where wrong. How does an LLM "learn" from incorrect proofs that it has generated itself? What does it learn? Can you explain how this mechanism works?
I’m not familiar with this specific example (or Mathematics) but I assume they keep intermediate results (python functions, lemmas, computations, intermediate proofs etc.) and formulate and explore adjacent ideas. Even with a failed attempt you can learn things. LLMs make a difference here because they can evaluate an experiment and hypothesize what went wrong or what should stick. So the search space is dynamically evolving unlike pre-LLM algorithms.
Karpathy’s Autoresearch provides a proof of concept for this method.
I don't agree that LLMs can evaluate an experiment. There's nothing in LLM training that makes them capable of telling what is e.g. a correct hypothesis from an incorrect one. I know that is a common claim particularly encouraged by AI companies but whenever that claim has been studied systematically and carefully the result is that self-verification doesn't work. For example, see:
On the Self-Verification Limitations of Large Language Models on Reasoning and Planning Tasks
https://arxiv.org/abs/2402.08115
Note also that basically all the mathematical results published so far have to be checked by an external verifier, either human mathematicians or a proof assistant like Lean, or both, and some systems explicitly couple an LLM generator to a traditional solver, like e.g. AlphaProof. None of this would be needed if LLMs could really evaluate their own results in any reliably correct manner.
An empirical paper from 2024 that doesn't give a principled reason why LLMs will always be bad at self-verification.
Which is to say, I think your criticism is unfair and an attempt to avoid engaging with the arguments in the paper.
In a way, yes. You can easily write a program that recursively enumerates all provable theorems in some order. But if you want a proof of a specific theorem, how do you find it in the list? You need to encode the theorem in a formal syntax first, and since mathematics is built on towers of definitions referencing other definitions, that alone is a significant amount of work before you can even write down what you want to prove.
If you want brute force alone, specialized solvers are likely a better choice than LLMs, but what LLMs add to the table is the ability to work with mathematics as it has already been written down. And even though they're bad at brute-forcing, they're still better at it than humans.
An example of a good division of labor is the SAT Attack on Tarski's High School Algebra Problem https://arxiv.org/abs/2608.08421 where they construct a formula with O(n⁴) variables and O(n⁶) clauses and use a SAT solver to show that it is unsatisfiable for n ≤ 11 but satisfiable for n = 12. Then they use an LLM to help them write a Lean proof that the SAT solver input is equivalent to the human-readable description of what they wanted to prove.
My current framing of this is that the advantage of LLMs lies in their ability to generate the text of a proof without having derived each of its steps in order, like a theorem prover (automated or not) would have to. There's nothing forcing an LLM to derive conclusions from premises (or indeed making it at all capable to do that).
They don't have to understand what the proof they generate means, or to be able to tell whether it's true. In fact, they can't do either. But that's fine as long as it's possible to check the proof with an external verifier.
So most LLM-based proofs use the LLM as the generator and an external verifier as the tester, either a solver like Lean or a mathematician. That's the best of both worlds as far as generate-and-test goes. A powerful generator tied to a powerful tester.
EDIT: yeah, like this:
>> An example of a good division of labor is the SAT Attack on Tarski's High School Algebra Problem https://arxiv.org/abs/2608.08421 where they construct a formula with O(n⁴) variables and O(n⁶) clauses and use a SAT solver to show that it is unsatisfiable for n ≤ 11 but satisfiable for n = 12. Then they use an LLM to help them write a Lean proof that the SAT solver input is equivalent to the human-readable description of what they wanted to prove.
I'm not disergarding the fact that LLMs don't generate text completely at random. They generate likely text. I suspect that can make it more likely to generate the text of some correct proofs. But I have no idea how likely that "more likely" is or what proofs are those.
Now LLMs have produced multi-thousand line Lean proofs. This is impossible by simply "try everything and see what sticks". LLMs are able to target their efforts to only promising proof strategies. Yes it helps that they work at superhuman speed, so they can try thousands of strategies where a human might try a dozen. But their results cannot be explained only by compute increases; they need genuine mathematical insight.
It depends what kind of automated theorem prover we're talking about. I'm not an expert on proof assistants like Lean. I am an expert on Resolution-based automated theorem provers and those can be implemented efficiently. For example, the SLD-Resolution based theorem prover used as the interpreter for Prolog (the logic programming language) runs in linear time and the cost of completing a proof is dominated by the cost not of the prover itself but the complexity of the theorem that is being proven. In more plain English when you run a Prolog program the cost that really matters is that of the program, not of the Prolog interpretation.
Now, I know that Resolution-based theorem provers aren't typically used in the same way as proof assistants let alone LLMs; but that is more of a historical accident than a limitation of the technique. There's no reason why one couldn't search for a proof of the Riemann hypothesis expressed as a Prolog program and using a Prolog engine. It's just not where most peoples' heads are these days.
>> Now LLMs have produced multi-thousand line Lean proofs. This is impossible by simply "try everything and see what sticks". LLMs are able to target their efforts to only promising proof strategies. Yes it helps that they work at superhuman speed, so they can try thousands of strategies where a human might try a dozen. But their results cannot be explained only by compute increases; they need genuine mathematical insight.
I understand the argument and I believe it has merit, but that's just to say that LLMs are trained to generate likely text, like I say in another comment. That is enough to explain the much improved ability to search quickly and efficiently (the LLM just has to generate text that looks like a proof; no need to actually carry out the steps of a proof) without recourse to 'genuine mathematical insight'. Which should be easy to believe because it's much harder to explain what 'genuine mathematical insight' is and where it comes from than it is to explain where the ability to predict likely text comes from: it's how LLMs are trained.
"A novice was trying to fix a broken Lisp machine by turning the power off and on.
"Knight[, one of the principle designers of the Lisp machine], seeing what the student was doing, spoke sternly: 'You cannot fix a machine by just power-cycling it with no understanding of what is going wrong.'
"Knight turned the machine off and on.
"The machine worked."
I feel like AI is manifesting this even more concretely. I don't feel like I'm guiding the AI super intensely as I work on it with software engineering. I'd have a hard time pointing you at where in the prompt my decades of experience are manifesting. But I definitely can have better results, even with a less frontier-level AI, than people who don't know the same amount of stuff.
Terence Tao also released some unedited transcripts of some of his conversations with AI, and many people observed that while many mathematicians may have been able to formulate the initial question, very few people could have given the same feedback to the AI.
Perhaps someday AI will eliminate the need for competence to use it properly. But that day is not today. And to be honest, that tech is probably not LLMs, no matter how large they get. Some other breakthrough will be necessary to truly eliminate the human element. Those psychopathic elites making plans to turn Earth into one of the Spacer worlds from Asimov's works with a small elite population supported entirely with robots take notes... it's not possible yet.
two hard things in computer science
https://blog.est.im/2026/stderr-04
I think LLMs are reall good at conjecturing based on existing knowledge, but inventing new tools/lemma and new paradigm? Not really.