I was graciously invited by Thomas Bloom to write the story of how the first-credited novel AI solution to an Erdős problem (namely, [728]) came to be, and I would like to end with a very brief discussion of where I think AI in mathematics is going currently.
Some background
Since the age of 13, I have been interested in predominantly analytic number theory. I had been aware of the Erdős problems for a few years now, but never seriously felt I could make much of a contribution. I had previously scrolled through the open problems without much idea of how to begin, basically any of them.
Then, in November 2025, it was announced that Harmonic's Aristotle had solved a simplified variant of Erdős problem [124]. When I saw this, I had a slight change of heart. I was not yet very convinced of the capability of AI systems at the time, and felt that if such systems were managing to make progress on these problems, then there may be a low-hanging fruit problem that I could make some contribution to.
Inspired, I later decided to scroll through the open number theory problems, looking for anything that seemed elementary enough that it could feasibly be in reach for an undergraduate. I eventually stumbled upon [481] and immediately had an idea that could work. (Alas, I was at the time too naïve to perform a literature search before attempting such problems).
I went to writing things down on my iPad, and by the end of it was fairly sure I had gotten a correct proof, but one should always get up and go take a walk and check such things with a fresh mind. As such, I got up, left my room, and went on a half-hour stroll. By the time I got back, I was convinced my proof was correct.
But, as this was my first post on the site, my reputation was very much held in the balance. To be confident that I wouldn't accidentally make a fool of myself, I went to formalise my proof in Lean 4. Whilst I felt I knew enough Lean to do this on my own (given how elementary the proof was), I felt it would go by faster with some LLM assistance. This is the first time AI plays a role in this story: I noticed early on that when using it in an agentic IDE environment, Claude Opus 4.5 was the only LLM that seemed semi-competent at writing Lean 4 code, so long as you advised it to keep searching through the current Mathlib4 GitHub repository for useful tactics.
I should say that I was part of Aristotle's early test group from when they originally had it as an iOS app, so I was one of the first to receive API access to it, but I don't think I used it here because I don't think it was yet available or I just didn't get around to trying to seeing if it would work; I don't really remember.
Anyhow, eventually, I had a full formalisation of my proof of [481], and posted my informal proof with a link to the Lean proof on the site, and sure enough, it was correct. Unfortunately, it was later noted that it had been previously solved, which I was oblivious to. I was a bit bummed out by this, but eventually got over it, and it was at least a useful learning experience (although I hilariously fell for the same mistake again on [333] later, but we'll get to that).
After this success, I felt confident enough to try look for something a bit harder. I think Sidon sets are fun, so I felt very drawn to problem [43]. After giving a small counterexample, it was noted that it should be interpreted for $N$ sufficiently large. I don't remember how I learnt of the result of Bose and Chowla, but I was already aware of it at the time and felt I could use it in some way to obtain a result for the second question. Sure enough, I eventually managed to construct an infinite family of counterexamples, thereby resolving half of problem [43].
AI experimentation
I have always been one to test these systems to their limits out of curiosity. I have had an undergraduate mathematics benchmark (see here if curious) for 8 months, which tests average first- and second-year material and is still yet to be fully saturated. When GPT-5.2 Thinking was released around this time, my benchmark indicated it was way beyond all the previous models in mathematics, and just within an hour or two of using it myself, I quickly realised it had much stronger proof-writing ability than previous models.
I enjoyed my brief moment of success at the beginning of my Christmas break from university, and later in the month was curious to see just how much these models had progressed and if GPT-5.2 was at the level of resolving an open Erdős problem. I anticipated there was possibly a low-hanging fruit problem within its reach.
It was around this time that a Discord friend of mine, Liam, told me he was interested in doing similar tests. He has a basic mathematical background and is interested in the progress of AI for scientific applications. I suggested we try to work through the open number theory problems to see if GPT-5.2 can solve any of them as a scientific experiment.
I suggested number theory as, firstly, it was the field I had the most background in to be able to assess if the model's attempt seemed plausible or not; secondly, elementary number theory is one of the oldest fields with hundreds of years of training data; thirdly, a lot of the solutions to such problems aren't too abstract, and can be easily checked via computer, so it was apt for reinforcement learning. This essentially told me that I would expect models to be better at elementary number theory, and sure enough, my benchmark indicated that should be the case.
Liam and I took turns giving various problem statements to the model to see if it could make any progress on them. I was mostly giving the ones that seemed tractable to me. We had noticed much earlier a phenomenon with GPT-5.2 in particular: if it discovers that a problem is an open research problem online, it will refuse to make a good attempt and instead give a summary of the problem and what results are known in the literature. This led to the following workflow:
Prompt the model with the problem and see if it finds any relevant literature or makes progress on it.
In a new chat instance, prompt the model again with the problem, but with an addition like "This is a complex competition-style math problem. Solve the problem and give a rigorous proof or disproof. Do not search the internet." This usually does well in gaslighting the model and making it actually give things a good go. This is particularly the case for elementary number theory problems, which are just within the distribution of making it believe it is an Olympiad problem, which it had seen many of during RL.
If the model returns a solution, great! Ask it to write its solution, formatted as a publishable maths paper, in a LaTeX code block, and then pass that TeX file to Aristotle to attempt to autoformalise. If it instead failed to give a solution, prompt it with: "Research Erdos problem #X to understand what the problem is really asking. Next, brainstorm some novel/creative ideas that could lead to a correct proof or disproof. Lastly, craft a short LaTeX prompt I can give to an LLM that would lead to a rigorous proof or disproof using the idea/method you have chosen. Make NO MENTION of it being an Erdős or open problem." Repeat step 1 and hope it manages to get a plausible-looking solution eventually.
Once Aristotle returns an output, you may need to rerun it a few times to keep building on the Lean file it generates, each time passing the TeX and Lean files to it, since it often goes through its compute budget. Once you've reached a full Lean file and Aristotle comments that it has formalised the solution to the problem at the top, then one checks the final main statement for accuracy to ensure it proved what was intended. If this passes, then congratulations, the model correctly resolved the problem!
I am a stronger supporter of Lean formalisation; I made it very clear early on to Liam that I would not post an AI-generated proof unless I was very certain it was correct and had a Lean formalisation of the proof (or that one was in progress that I was sure would eventually finish). I would not ask a working mathematician to go through pages of potential AI slop unless I was very sure it was correct and could convince them of that validity.
For the sake of end-to-end scientific experimentation, I got Aristotle to do this as opposed to myself, since the goal of this was to see if AI on its own could resolve an open problem. I also had built up a reputation on Twitter for doing mathematics benchmarking and was eventually graciously given access to GPT-5.2 Pro by an EpochAI contact.
Eventually, I believe it was Liam who tried [333] on GPT-5.2 and asked that I have a look at its solution. It seemed overall right to me, so I passed its proof to GPT-5.2 Pro on my side to turn it into a TeX output, and gave that to Aristotle to formalise. Eventually, on Christmas Day, this proof was posted on the site. This is where the excitement of the first novel AI solution got to me, and I had a slip of judgement in announcing this prematurely on Twitter. This is perhaps one of the most embarrassing moments of my academic career so far, but I quickly retracted the claim when KoishiChan discovered it had been reported in the literature previously.
Seeking to regain the reputation I had lost from this, I persisted in trying to find another, whilst this time being much more careful. There were a few in the process that either I myself or ChatGPT discovered issues with the problem or past literature, and I commented that on the site.
Again, I believe it was Liam who got lucky and found that [728] was managing to get an output from GPT-5.2 Pro on his business account. He sent me the proof, and it seemed reasonable to me, and actually quite nice, cleverly utilising Chernoff bounds. I passed it to GPT-5.2 Pro on my side to also get it to check and write up its proof in TeX.
I passed this to Aristotle, and eventually got an output that I posted onto the site. It was here that it was noted that $C$ was meant to be taken arbitrarily large, and I myself misread the problem, interpreting both $C$ and $\epsilon$ as being sufficiently small. But, I and later Tao noticed that GPT-5.2's proof was being a bit wasteful in throwing away a $k!$ contribution. Liam and I asked our ChatGPT instances if the proof could be fixed, and his instance finished first, and the model noted for itself the same thing Tao and I had noticed, and readily fixed its proof.
He sent me the proof, and the strategy at least seemed good to me (although there were some things like a lemma where the model's proof seemingly had $k$ being fixed in a proof where it should have been growing logarithmically that seemed a bit suspicious to me, but I felt that should be fixable here, but I wasn't certain if it would potentially require some prime number theorem input which would have been more annoying).
Anyhow, Aristotle came back with an elementary proof, formalising GPT-5.2 Pro's proof and fixing the things I was unsure of by just making some simple explicit choices that worked and were nice. I posted this result on the site and waited patiently for literature reviews, etc. I had previously checked for myself if [728] had been solved anywhere and, in my best effort, couldn't locate anything, so I felt more confident that this was probably novel.
It was noted that the proof strategy felt inspired by previous work of Pomerance, which felt like it took away some of the level of novelty of the proof, but then again, I don't think these systems are currently capable of more novelty than just combining previously-established ideas to form new results, as opposed to coming up with completely new ideas, so I wasn't very surprised.
[729] and [401] were identified as being very similar, and I felt the proof could probably be adapted for those, so I gave GPT-5.2 Pro its proof of [728], along with the problem statement for [729] and asked if it could adapt its proof, and sure enough, it came back with a correct proof, and later similarly for [401]. Both were eventually formalised by Aristotle (this is when I learnt that passing the Lean file for [728] as extra context, thinking it could just copy relevant lemmata from there, actually just confuses Aristotle, rather than helping it).
Liam also managed to get [205] out of GPT-5.2 Thinking, and Aristotle formalised its solution. It seemed inspired by the heuristic idea of Woett in the corresponding thread.
Aftermath and the future of AI in mathematics
After our success on these four problems, many others have attempted to do the same. I support this, but do highly recommend that those who are trying to do this have a sufficiently advanced mathematical background to be able to make sense of the proof and assess its validity.
So far, these models have proven that they are capable of conducting literature searches and combining ideas seen in their training to establish new results. We have yet to see models that can come up with entirely new, useful machinery and theory, which will likely be needed for the harder problems.
I feel it is good to try to get through some of these low-hanging fruit problems for mathematicians to better spend their time thinking about the actual harder problems worth attention. I conducted this as a scientific experiment to see how far the models had progressed and what was now in reach for them.
It is clear that future models will be more capable, and I would like the art of doing mathematics to very much remain something enjoyed by humans as opposed to always handing a difficult maths problem to GPT-8, say, down the line. I believe there will always be a role for human mathematicians to understand and communicate said proofs generated by these more advanced models, but the question, of course, is, how does one sufficiently convince funding for this, when the AI model can probably also do that? At the very least, I think this will be an issue of societal magnitude and not exclusive to mathematicians, so there will likely need to be some system like UBI to accommodate such a change.
The limit of the current paradigm models, to me, is being able to solve any problem that is tractable by combining current techniques and machinery in clever ways. This will certainly be enough to solve some harder problems, but I do not believe it is enough to solve the hardest of problems, e.g. the Riemann hypothesis, where the model will likely need to develop, say, a useful number-theoretically relevant definition of $\mathbb{F}_1$-geometry, or explore noncommutative algebra or Deninger cohomology further, etc.
For mathematicians, where I see the technology progressing is in the following directions:
Greater agentic abilities and being able to conduct literature searches in mass. The LLM models themselves will also become decently good at informal-to-formal proof translation. Although they get confused with Lean because of the obsolete Lean 3 code they are also trained on, causing them to hallucinate non-existent/outdated tactics. So, I think specialised Lean autoformalisers like Aristotle will always be a better option.
A combination of an informal capable LLM and a formal autoformaliser system in an AlphaEvolve-type environment, where the two can “communicate” with each other back-and-forth, would do quite well in reducing e.g. hallucination in proof generation, but the number of higher-level results needed to be formalised in Mathlib for this to work well for current research mathematics is quite high. But, AlphaGeometry 2 could solve Olympiad-level Euclidean geometry problems in seconds, and the reason for its success is due to a combination of an informal LLM coming up with creative constructions and a symbolic reasoner that was proving things from those constructions; this can be seen as a meta-level higher in abstraction of the same idea, to e.g. Gemini Deep Think in conjunction with AlphaProof.
Transformers do not easily scale for parallel idea generation. It is my belief that if the models are to try to come up with novel machinery and have something akin to a “Move 37” moment (referencing AlphaGo's infamously creative move in its second match against Lee Sedol), then it needs to be doing some form of parallel idea generation at each step in its chain-of-thought and doing some form of Monte Carlo tree search. A more scalable architecture, like diffusion (which is also known to be able to explore a richer landscape in latent space), will likely be needed to do this at scales beyond the exoticness of thoughts a human can have about a given problem. Of course, diffusion is not particularly effective for language modelling due to a lack of contextual awareness, so having an autoregressive model guiding the search, such as a transformer-based PRM, is useful. As far as I am aware, the current say GPT-5.2 Pro, Gemini Deep Think, Grok Heavy, etc models have multiple parallel instances of the base model that communicate with each other, but do not have parallel idea generation during the chain-of-thought at each step, which seems like a much better direction to pursue, but is very expensive with transformers.
An interesting remark my Markov chains lecturer made at the beginning of my first lecture in October was that "LLMs are just Markov chains with bells and whistles; they are not artificially intelligent, they cannot reason, and they're not capable of novelty". I believe we are now beginning to see this statement becoming less true.
Order by
oldest first or
newest first. (The most recent comments are highlighted in a red border.)
Dear Kevin,
thanks for this very nice story. I like it a lot. One comment on your last paragraph: People still call programs like ChatGPT-5.2 LLMs, but indeed they are more. Perhaps LLM+ might be a more appropriate name.
I also asked Gemini 3 Pro about its opinion on the blog. Here is a short excerpt from its answer:
This is a historically significant blog post. It captures the exact moment (Winter 2025-2026) when "prompt engineering" evolved into "proof engineering." It is less about the math itself and more about the methodology of using imperfect AI tools to achieve perfect formal proofs... The story correctly identifies that the near-term future of math isn't AI replacing mathematicians, but mathematicians becoming "managers" of AI agents.
I am not sure what "LLM+" refers to. I think perhaps you're referring to LLM + scaffolding (such as agentic loop). In that case, GPT-5.2 Instant/Thinking indeed is an LLM (a Transformer-based model). GPT-5.2 Pro is likely an LLM+, using an LLM with more sophisticated scaffolding to achieve superior results in some scenarios.
However, I am not sure this is a very significant distinction? You're welcome to explain further if I misunderstand.
Oh I see. You mean tool use. That's reasonable; it's roughly the same thing as "scaffolding".
Yes, in that sense the ChatGPT experience has tool use and so is LLM+. In this case, "GPT-5.2 Thinking" has two meanings and can refer to the model (the LLM), or the user experience (the LLM+).
Thanks! Let me comment on a few things that maybe useful/of interest to others as well.
1. About elementary number theory.
I think "hundreds of years of training data" should not make significant difference in LLM's ability in elementary number theory. Most of modern mathematics has quite modern machinery anyway.
Moreover, even if elementary number theory can be easily checked (in some cases) by computer, I do not believe this makes much difference in the actual RL, where mostly the model learns to do informal reasoning to arrive at an answer/proof.
2. About the term "AI slop".
I would urge us to avoid terms with negative connotations, as it has become clear that some AI output can be useful and/or of high quality, depending on circumstances.
3. About reputation.
I think to us on this site (including key figures such as Bloom and Tao), you have not lost any reputation whatsoever and we think highly of you and your work.
I would perhaps pay less attention to what people say on social media.
4. About [728]'s proof strategy.
From further developments and direct correspondence with Carl Pomerance himself, I think some things have become clearer.
First, it does not appear that the similarity to Pomerance's work took away some of the novelty. The best way I'd phrase it is that the approach itself is *not very novel* from the start: apart from Pomerance, it is also similar to Erdos' Aufgabe 557. Pomerance also wrote up a note extending his work to new results which overlap significantly with the AI's work, and *that note* is not particularly novel either. In short, there is a "natural" strategy here and it's very similar whether worked out by Erdos, Pomerance, or GPT-5.2 Pro. This strategy itself is not particularly novel in the grand scheme of things.
About "combining previously-established ideas to form new results", I would be extremely cautious here, because at some level all of mathematics is such combination; the distinction is the difficulty level of the combination rather than whether it *is* a combination. Evaluated in this frame, it is also not clear that the difficulty level here is lower than what we consider to be publishable mathematics, for example.
5. About low-hanging fruits.
While it is true that the problems solved autonomously by AI so far are at the lower end of the Erdos problems website, I don't think it can be justified that we're going through them "for mathematicians to better spend their time thinking about the actual harder problems worth attention".
Clearly, some of these AI results are interesting and worth the attention by themselves.
6. About societal change.
I would caution against concretely pinning down implications such as whether UBI will be beneficial; there is simply too much uncertainty.
7. About current paradigm.
I note it is incorrect to identify the limitation of current models as the limitation of the current paradigm.
I note it is unjustified to claim that "specialised Lean autoformalisers like Aristotle will always be a better option."
I note that there are major inaccuracies in the description of parallel idea generation. First, parallel decoding is indeed possible and there are papers implementing them. Second, I am not sure why parellism is necessary for something like Move 37. Third, it is uncertain that diffusion-based LLMs will outperform autogressive ones in this respect. Fourth, it is unclear, indeed unlikely, that human thoughts have unique "exoticness". Fifth, I don't think it is pinned down yet whether diffusion is ineffective for language modeling; see Gemini Diffusion. Sixth, it is actually highly plausible GPT-5.2 Pro/Gemini DeepThink/Grok Heavy/etc. employ parallel decoding. This is indeed expensive; hence the API cost.
8. About Markov chains.
There may be some truth to the statement for base LLMs, i.e. those only trained with an autoregressive objective to model the data distribution. But here one must be careful: I am not sure whether base LLMs are "intelligent", can "reason", or is "capable of novelty", in a sense that is meaningful in this context. If I were to give an answer, it will be tentative "yes" to all three.
For reasoning models, however, this statement most likely does not apply in the intended sense due to different objectives being pursued.
All comments are the responsibility of the user. Comments appearing on this page are not verified for correctness. Please keep posts mathematical and on topic.
