It is often overlooked how expensive these models can be to run, and the false positives or other dead ends. You are going to be burning through a lot of $ if you use the latest models on hard problems, with no assurance of progress...
For a list of AI accomplishments in mathematics see https://mathoverflow.net/questions/502120/examples-for-the-u... - or a candidate list here: https://aimath.robertj1.com/ . Many have observed an affinity of AI to the search for counterexamples - or examples. Looking at afore lists, something much more sociological crosses my mind: There is a hunt for answering prominent, clearly stated problems. I'm not a mathematician, but is this mostly what progress in mathematics is about? How about stating worthwhile problems in the first place? What about theory building? Am I right saying this is equally important, but none of those utilizing AI for mathematics seem to be interested in such?
> 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.
There’s a well-known essay from the 90s where Timothy Gowers predicted that the creative/intuitive side of mathematics would be entirely taken over by machines before 2100.
Since no one has mentioned it yet - just want to point out that Timothy Gowers is a Fields medalist.
Given coding agent's demonstrated difficulties with concurrent code, even relatively simple concurrent code, it would be interesting to see how they do with temporal logic. I don't know enough to throw AI at the problems in that space but I wonder if they wouldn't crash and burn on it.
(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 thoughtful and measured post, as usual from Gowers. The final note is neat and worth pasting out here in full:
> 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.
How i reason about this is that, there are two types of science works, exploitative and generative. Exploitative science is kinda like what ingen do in jurassic park, finding an use case based on available tensions in the literature.
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...
> If they were, then their big speed advantage over us would mean that there would be much more of a flood of results.
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
Correct me if I'm wrong, this is not the right way to ask this question.
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).
Increasingly, I've begun to think of LLMs as sources of really interesting random objects: large pieces of "reasonable thinking" conditioned on a task. It's not that these are correct, in general, but instead they're a concentrated form of random search where that "randomness" is very likely to follow plausible, human patterns.
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.
If you want to peek inside how a model solves a math problem have a look at some data visualizations I made solving basic multiplication.[0]
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.
It seems intuitive that finding a counter-example might be easier than proving a generality, since you're starting from a concrete goal ("build a foo that has properties X, Y & Z") that you can branch out from, identify sub-problems, etc.
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.
The biggest win for AI dev efficiency is cutting down what gets loaded into context. Semantically matching tasks to the top tools helps a lot.
Disclaimer: I only scanned the article quickly; I might be re-stating something already in the article.
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.
___________
From my experience, you have to be good at math to trust an LLM to do the math.
They are exceptional at the spending cost math :)
[flagged]
[flagged]
[dead]
How interesting is it that in the same way the human brain unconsciously does calculus and linear algebra, but struggles in the conscious space (we have to go learn it, it’s not easy) the same is true of LLMs.
They are algebra, and yet kinda suck at it without training
This is really an argument about test-time scaling, even though the post never uses the term.
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.