On one particular Friday afternoon, he stated a conjecture that he hoped was true, and invited us to try to help him prove or disprove it. It was the sort of thing that he really wanted to be true; he liked things smooth and beautiful. I, on the other hand, hoped it was false as I like the weird and exceptional in mathematics. It was also the case that I had absolutely no command of the sort of machinery that one would use to prove such a thing, but I could certainly look for a counterexample.
I learned on Monday that he had spent the entire weekend trying and failing to prove it. I, on the other hand, had put all my energy into finding a counterexample and had one within an hour.
My single (quite small) contribution to mathematical research was a counterexample because it was all I could do. The story does illustrate that it can be helpful to have people with different tools, hopes, and motivations working on a problem, though. I was not, and will never be, even a shadow of that great mathematiciam I studied under, but on that occasion, I had reason to look in a different direction than he did.
1) I recommend the wonderful 1976 book Proofs and Refutations by Imre Lakatos.
2) There is a considerable list of books dedicated to counterexamples, e.g. in topology, probability, analysis, etc.
Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.
Interestingly, Yitang Zhang of the twin-prime-conjecture fame spent 7 years working on the Jacobian conjecture under the advisor Tzuong-Tsieng Moh at Purdue. A key step in his thesis used a corollary of Moh's. It turned out that the corollary was incorrect. As a result, Moh refused to write any recommendation letter for Zhang, and Zhang couldn't find any teaching or research job and ended up spending years working at a Subway[1].
Imagine Zhag had ChatGPT in 1986 when he started working on the Jacobian Conjecture.
[1] Of course now this has become an inspiring story. That said, the story definitely invokes complex emotions. The best way to describe it is probably this Chinese poem, which I have no idea how to translate: 庾信平生最萧瑟，暮年诗赋动江关
Yeah, given how much it accelerates grad students to produce meaningful output more quickly, why wouldn’t you make an investment of $2400/student/year. Seems like pennies overall.
One thing that he mentions that already quite surprising is that AI was able to autoformalize the Golod-Shaferevich theorem and proof.
Hm, as a mathematician, my experience feels opposite. A proof would be an adaptation of a proof I know, some tweaking it here and there. A counterexample would require some deep understanding of the structure of the objects involved, which frequently is beyond my comprehension.
But probably this is because I think of quite abstract objects which are harder to grasp. For numbers or polynomials, this would be the other way round.
P.S. It helps that in CS lots of theorems are about either inductive or coinductive definitions.
and for now as long humans are going to judge of what counts as an elegant or illuminating proof, there's going to be work for human mathematicians
It's not easy to find a counterexample to the Jacobian conjecture, by any means – by which I mean to say that naïve brute-force search will take too long – but the scope of existing searches listed on Wikipedia[0] suggest that many tricks are already known, and that people just hadn't looked, systematically, for a counterexample in three variables before. Wikipedia writes:
> Tzuong-Tsieng Moh checked the conjecture for polynomials of degree at most 100 in two variables.[17][18]
where reference 17 is from 1983, and reference 18 is a preprint with no given date. Knowing very little about this problem, my impulse is to side with the unnamed faculty member cited in the article:
> [who] said to me that the fact that the counterexample was so easy to find just indicated that humans had not spent enough time thinking about the problem,
For context, the auto-generated counterexample is in three variables, has degree 7, and was discovered in 2026.
There's no structural reason to expect acceleration any more or less than an asymptotic behavior (if even that, acceleration is probably the bigger ask). Different problems yield to a new solvent, maybe that's also more, but it could go either way and we definitionally don't know yet because we don't understand the convexity of AI capability, we cannot directly access it interiority, we don't know if it's sandbagging (other than that it does sometimes, it can). It's an emergent phenomemon that might actively resist measurement. Or it might be as predictable as a clock in a few years.
No one knows, or if they do, they aren't talking. The loud people don't know anything.
I'm tired of tales like this in academics though. That's not a criticism of you for telling the tale, I'm just so tired of this kind of thing in academics in general. So, so, so much politics and public reputation management. Zhang should have never had to suffer like that.
As my own research has drifted more into math, I've been surprised at how many assertions in the literature turn out to be false. Not just false, but propagated into the applied literature extensively, and even when you point out the problems a lot of defensiveness and denial about it along the lines of Zhang's story.
I agree about wondering what would have happened if LLMs had been around in 1986. My guess is the outcome would have been the same for the same reasons?
My experience with LLMs in proofs is they can be very helpful, but also very wrong. It's like having another person with another set of hunches about what path to go down.
Yu Xin’s was a life of utter desolation; in old age, his poems and rhapsodies stirred the riverlands.
The conjecture had to do with whether one convex polygon could be continuously deformed into another while remaining convex, under certain conditions and constraints. The answer turns out to be no, but surprise and disappointment are understandable reactions to that outcome. It was indeed much more practical for a young grad student to look for a clever misbehaving polygon than to try to prove something about all of them at once.
He spent an entire weekend before having the wisdom to pause, and let someone else contribute their time to finding a counter.
Also, 'brute-force' style attacks where one simply feeds the input into the computer and it yields a solution are nothing new and certainly predate LLMs: https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...
Hell, one could even go further into the past and refer to the thankless work of pre-computer era mathematicians who sweated over manual calculations in order to disprove various prime related conjectures: https://en.wikipedia.org/wiki/Mersenne_conjectures
You seem to have an objection to non-intutionist mathematics in general, a position that was once held by many an illustrious mathematician but is relatively fringe in the contemporary academic community. Mathematical facts don't have to be intellectually satisfying or make sense to you, the human, rather it is up to you to wrap your mind around discovered mathematical facts.
Couldn't people in principle continue to study a problem that's only been shown to break at one point? Prove something adjacent, or slightly weaker, or elaborate the counter example into a powerful explanatory framework?
If we do it probably won’t be for a long while. We’re barely using math from a couple hundred years ago for most applied usage.
The difference today (and the reason why everyone is excited about it) is that the same system that does advanced math can write poetry, play an above average game of chess, code frontend/backend stuff and do cybersec. These are not "expert systems", nor are they trained for each task individually. That's the catch.
> just indicated that humans had not spent enough time thinking about the problem
Heh, this is a weak excuse. We've seen variations on this theme every time something cool gets solved by the models.
[Dis]proof by counterexample is the most straightforward way to show a statement to be false. What better way is there to disprove a general statement like 'all x are y' than finding an 'x' that isn't 'y'?
Maybe the prompt contained a part like this: "the search space is too big to just try all the combinations of 3 variable polynomials, so be clever about it". Or maybe this part was omitted from the prompt, because modern LLMs are smart enough to figure this out without us having to mention it.
https://aaronlou.com/jacobian_counterexample_prompt.pdf
Obviously it is not random, but it's very generic. No mention of search space or how to reduce it.
A PhD student discovered that a result of his professor would imply the solution to a big conjecture in another field. The people in that field then analyzed the prof's result and found that the proof was flawed. The student was still allowed to graduate based on this since the finding of the connection between fields was brilliant. Then he quit academia (not because of this story, he had planned it before). Then a year later the prof figured out how to fix the flaw in his proof and published a paper with his former student, thus solving the conjecture. The two are still on good terms, writing papers together.
No life ran more bleak and desolate than Yu Xin's —
yet in his twilight years, his verses stirred the rivers and the passes.
Very true. Unfortunately, when there are people, there will be politics. I remember when reading Yau's autobiography, I kept marvel how much calculation, or "politics" if you will, that Yau mentioned or implied in the book.
> My guess is the outcome would have been the same for the same reasons?
At least Zhang didn't have to spend 7 years working on the Jacobian conjecture. He said in an interview that he always wanted to work on number theory. Moh asked him to work on Jacobian, and he obliged.
In his exact words: "A new scientific truth does not triumph by convincing its opponents and making them see the light, but rather because its opponents eventually die and a new generation grows up that is familiar with it... An important scientific innovation rarely makes its way by gradually winning over and converting its opponents: it rarely happens that Saul becomes Paul. What does happen is that its opponents gradually die out, and that the growing generation is familiarized with the ideas from the beginning: another instance of the fact that the future lies with the youth."
And he said that having lived, as a outsized figure, through the late 19th to mid 20th century of physics, which was the absolute golden age for such.
Unless you want to spend time "proving" that 2 * 2 = 1.
Occasionally large improvements in our models of the universe have been associated with the development of mathematical tools that allow those models to be expressed and/or tested.
Considering ChatGPT was released only three and half years ago, and LLMs could do high school math only less than two years ago, I think this "for now" will not last very long.
We're a good team, and that's ok.
Naomi Wolf 'death recorded' on BBC[1], skip to 5:51. After this the book was pulped and she had some sort of psychotic break during COVID and allied with ultra-right and COVID denialist loonies.
Yu Xin's past was exquisitely tragic
Ages passed; now his works betray magicThe professor was John Milnor.
They are explicitly trained for each task individually.
That makes sense. She wouldn't want to be burned by people doing fact checking again. Write books for the crowd that will never do the legwork to discover that you're full of shit.
> After this the book was pulped and she had some sort of psychotic break during COVID and allied with ultra-right and COVID denialist loonies.
That's quite an extreme shift considering she had previously been a leading figure in third-wave feminism and an OWS activist.
But mathematics is not a collection of facts. Mathematics is the study of abstraction. And what do you learn from a single data point? What can you abstract from that?
That's why just being a counterexample isn't really interesting. There has to be more than "counterexample" for there to be something to abstract. Was it generated from an analysis of the problem? Can the counterexample be generalized to explore the problem further? Is the counterexample a surprise in a way that suggests something is missing from current understanding?
Being a counterexample doesn't mean that something isn't interesting to a mathematician. But it's also not the interesting part.
Sometimes, of course, the proof is just wrong. That is the dangerous case, which will cause either major corrections or failure.
We really need to stop thinking about LLM training data as the knowledgebase they build from and instead consider it more the skillset they start with.
Probably there are understandable reasons for that... But I think "negative science" is really important, and soft results like "we tried that for a long time and it wasn't very fruitful" are actually very important for progress even if they're poorly attested in the written record. I guess in mathematics they come informally from your thesis advisor...
More generally I think people are inappropriately confident in general. When you go through history just about every century prior people believed many things that the next century would come to see as plainly false. People in modern times seemed to have stopped believing this was true, yet it's likely that people during every given century also stopped believing such was true, because what you believe "now" is always assumed to be correct. Nobody wants to believe they hold false beliefs, even though there's a practically 100% certainty that all of us do, and in quite healthy quantities.
All we're able to do is apply flawed analogies, generic information theoretical models, trial and error, post-hoc rationalizations and benchmarks without really understanding why.
EDIT: just re-read your comment. I don't think you have a good understanding here, no offence.
Alice is a football stats wiz. Alice is a WR Jones fan because he has an incredible 40-yd dash time and leads the league in YAC.
Bob is a WR Smith fan. Bob knows the stats are all cooked. Bob knows that if the stats weren't cooked, WR Smith would lead the league in all categories. Therefore, Bob doesn't bother with stats.
*statements only apply to maps whose domain is finite-dimensional
It's understandably the natural place to get the dramatic tension from what at least purports to be a sober account with some momentum. It's reasonably consistent with the way it's treated on the lectures I've seen from Sir Andrew Wiles on YouTube.
It sounds like a nightmare. He had intentionally set the proof up in a high stakes way, working in private, very quiet on what he was really doing. I gather this is not the done thing, eccentric at best kind of vibes, and I think by that point it was almost crackpot adjacent to even try seriously. His advisor forcefully pushed him off even trying earlier. So it's compound on the stakes. The beg reveal is intentionally as dramatic as possible. And then the questions start to land, most are minor clarifications, notation deficits, but one is sticky, one won't go away.
Kept me up late reading about it.
I think the misunderstanding comes from "individually". You are thinking about diverse datasets, but that's not what individually means in this context. In ML individually trained means that for each task you prepare an architecture, dataset and eval and train that model on that data. And each model has its own objective that you train for. In LMs the objective is singular, for every data point - next token prediction. And, importantly, you train on every datapoint, the more diverse the better, but not independently. The cool thing is that training on diverse datasets improves scores on other downstream tasks, while the training objective is the same.
So you can have a training run on common crawl + programming that improves scores on logic puzzles, or common crawl + novels that improves scores on planning tasks. But the important thing is that it's all trained together, not independently.
> The cool thing is that training on diverse datasets improves scores on other downstream tasks, while the training objective is the same.
Maybe for some language modelling tasks, i.e. it learns some internal representation that is transferable. However I would find it quite odd if a model becomes good at Bio while not explicitly going through Bio training.
It’s been an interesting few weeks for counterexamples. This post is basically my perspective of what has been going on in the world of formalization, AI tools and, in particular, counterexamples.
Two months ago today (20th May 2026), ChatGPT disproved Erdős’ Unit Distance conjecture in discrete geometry. This is now old news but I had to start somewhere. The announcement was accompanied with testimonies by human mathematicians, many of whom I knew and a few of whom I trusted, saying that they believed the argument (they had been given early access to it and had checked it). The basic structure of the proof is that a profound theorem in number theory due to Golod and Shafarevich from the 1960s could be used to construct a counterexample to the conjecture.
It is now 9 years since I had a mid-life crisis, realised I no longer trusted many human mathematicians when it comes to technical details, discovered Lean, and started to argue that interactive theorem provers should play an important role in the future of mathematics. So of course my first question was “is the counterexample formalized in Lean”. The answer was “no”.
But under a week later (26th May 2026), I got an email from Fields Medallist Mike Freedman. Mike is now the Chief Science Officer for Logical Intelligence, a company cofounded by Turing Award winner and “godfather of AI” Yan LeCun. Mike informed me that their system had autoformalized the entire ChatGPT-generated paper in Lean and could I take a look. I looked, and my post-doc Thomas Browning looked too. And indeed this was what Logical Intelligence had done: they had formalized precisely the statement that the profound theorem of number theory implied the Erdős counterexample. Breakthrough LLM-generated mathematics being formalized in real time. Interesting data point.
Of course there is an elephant in the room here though, the profound theorem of number theory which takes 100+ pages to prove (it needs huge chunks of global class field theory, a theory developed at the beginning of the 20th century and for which there are still no short proofs; it is proving difficult to compress). In 2025 I had run a Clay Summer School with Richard Hill on the formalization of class field theory, and one year later we have nearly done the local case (it is the current PhD project of my student Edison Xie); the global case remained open, and indeed in 2025 formalizing global class field theory seemed like a fantasy.
One month later, on June 26th 2026, my perception of what was possible again changed. Boris Alexeev announced on the Lean Zulip that he had steered ChatGPT to a complete formalization of the Erdős counterexample, assuming nothing beyond the axioms of mathematics. Boris works at OpenAI and had used their new model Sol to do the autoformalization. Boris made the code public and it did not take long for me to realise that somewhere within all this AI-generated (and sometimes horrible, although sometimes decent) code was indeed a proof of some really hard theorems in global class field theory. Also of interest to me was that Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project. Lean’s fantastic (declaration of conflict of interest: I am a maintainer) mathematics library mathlib is only 2.3 million lines of code, and took nine years to write. Perhaps it was at this point that the penny really dropped for me — large AI-generated developments of mathematics are inevitable. One cannot trust AI-generated code so I ran it in a sandbox on my machine (malicious Lean code can run arbitrary commands on your computer — Lean is a programming language, after all). Indeed, it was proving nontrivial theorems about the cohomology of number fields. Wow.
A week after Boris’ revelation, in early July, I was thinking hard about how to run my Formalizing Fermat workshop. This workshop was sponsored by Logos Research, who, like Logical Intelligence (and Harmonic and Axiom AI and Moonshot AI and…) have a tool which can autoformalize mathematics — translating it from human language into Lean — building on mathlib. Logos told me that they were only going to allow 5 people at a time to use their system during the workshop, and there were 25 attendees, so I told all attendees that I would buy them a Claude Max subscription for a month, so they had something to experiment with when it wasn’t their turn for Logos’ tool. The workshop was 6th to 10th July, and the Claude Max subscription would give attendees access to Claude Fable, at least until Tuesday 7th, when it was being switched off. When OpenAI got wind of what I was doing, they also offered all attendees free ChatGPT Pro access for a month; this was a big deal because ChatGPT Sol was coming out on the 9th. So basically all attendees would have access to Sol and Fable for 4 out of the 5 days of the workshop, and Logos’ tool for the entire week. In fact Fable access was not removed on the 7th so we were in even better shape.
I was not sure how good Logos’ tool was going to be, but I wanted a development of the theory of finite flat group schemes in Lean for my ongoing proof of Fermat’s Last Theorem, so I put uploaded some classic papers in the area to Fable and ChatGPT, and got them together to write down an exposition of the theory in natural language. I passed this pdf document over to Logos the day before the workshop, and on the first day of the workshop they said that one of the claims in the pdf was false and they had found an explicit counterexample. Another counterexample! I took a look and indeed the LLM-generated pdf was simply wrong at some point when describing a standard construction; false alarm. I had missed this myself though when reading through the pdf. Interesting how AI had again found a counterexample. I fixed the pdf. I thought it was interesting that the AI didn’t just say “I don’t quite follow this argument”, it instead said “here is a proof that this argument is simply wrong”, a much more powerful statement.
With the development of the theory of finite flat group schemes back on track, I could relax back into the FLT workshop. On Tuesday 7th July I sat opposite Akhil Mathew at lunch; Akhil is a professor of mathematics at UChicago and he was an attendee who had been experimenting with the tools available. We talked about potential questions which AI could work on, and Akhil raised the old question of Grothendieck about whether every finite free group scheme of order n was killed by n. Deligne had proved the result in the commutative case, and Grothendieck had proved it when the base was reduced; Rene Schoof had proved it in more cases, and there had even been a paper by Emiliano Torti published last year, proving it in even more generality. I said that I thought that this was a fabulous thing to get AI thinking about.
The day after the workshop finished, on Saturday 11th July, I got a DM from Akhil telling me that Sol had found a counterexample. He sent me a 12 page pdf. I immediately replied saying that I was not reading AI-generated informal mathematics and could he please formalize the entire thing in Lean. Four hours later he replied again, saying that Fable had autoformalized the entire thing. I scanned over the 1076-line Lean file, checking that the code did not delete all the files on my hard drive (Lean is a programming language, so it can do this). Convinced that it was only theorems, I then compiled it on my laptop and it took me under 5 minutes in total to check that (a) the statement of the claimed theorem used only concepts in mathlib (and thus things like [HopfAlgebra](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/HopfAlgebra/Basic.html#HopfAlgebra) can be trusted to mean what mathematicians think of as Hopf algebras) (b) the statement of the claimed theorem was that there was a counterexample and (c) the proof compiled. At this point I knew that we had a counterexample — a group scheme of order 4 which was not killed by 4. I suggested to Akhil that he make a PR to mathlib with the counterexample — which he did. I would have also suggested to him that he draft a press release saying that a machine had solved a 60-year-old question of Grothendieck in algebraic geometry, but somehow by this point I was almost becoming immune to all of this. It wasn’t clear to me that the media would even be able to distinguish between “machine resolves question due to Erdős” and “machine resolves question due to Grothendieck” even though I personally found the latter far more interesting. Of course the Grothendieck counterexample was far far easier than the Erdős one (a thousand lines, not a million), all I’m saying is that it’s an area of mathematics that I personally find more interesting. I pointed out to Akhil that machines seemed to be getting very good at finding counterexamples and suggested that he try the Hodge conjecture next.
I think it’s worth stepping back at this point and surveying what the attitudes of human experts to these sorts of things are. On Tuesday (14th July) I went to work at Imperial and the Grothendieck counterexample was the talk of lunch. A member of the faculty (who I won’t name) said to me that the fact that the counterexample was so easy to find just indicated that humans had not spent enough time thinking about the problem, implying that a 60-year-old question of Grothendieck was not actually that interesting to work on. I didn’t tell him that at some point earlier in my career I had spent a week working hard on the problem. In my mind my colleague is just going through the five stages of grief; right now they seem to be in the denial phase.
After lunch I met with my PhD student Andrew Yang, who had been working on formalizing a modularity lifting theorem in Lean, something which is crucial to my FLT work. Andrew had come to the Logos FLT workshop and now had access to both Sol and Fable. He told me that using these tools he had written 250K lines of Lean code which basically completely finished the project in what was I guess a 2 week period.
A few days earlier I had got an email from a professor in the maths department here at Imperial, expressing surprise that some of our graduate students were paying $200 per month to access models such as Sol and Fable. He said that he thought that these people were crazy. I did not immediately respond. But after meeting with Andrew I emailed the professor back and told him that in my opinion, any PhD student who was not paying $200 per month to access these tools was crazy. In fact during the workshop I learnt from Harvard PhD student Bryan Wang that Harvard were already giving free Fable access to all PhD students, post-docs and faculty at Harvard.
But back to Akhil. I am not sure if he took my idea to disprove the Hodge conjecture seriously. But it looks like he had deeply understood that, with these extraordinary new AI tools, counterexamples might be low-hanging fruit right now. He had discussed with Levent Alpöge the idea of finding more counterexamples in algebraic geometry, and 12 hours ago Levent posted on X that Fable had found a counterexample to the Jacobian Conjecture. This is a big deal — this is a famous question in algebraic geometry which had been open for 100 years and which many people had thought about. It was apparently solved during the 2026 World Cup Final.
I woke up today to a DM from Akhil saying “shall I make another PR?” but this time he was too late — Paul Lezeau had already formalized the counterexample manually and had made a PR to DeepMind’s Formal Conjectures repo. Mathlib does not contain a large list of conjectures in mathematics, but DeepMind’s repo does. The importance of formalization of conjectures by humans is that if humans are agreed that a Lean statement does faithfully capture the idea behind a conjecture, then checking that (possibly AI-generated) Lean code does comprise a proof or disproof of the conjecture is a triviality. Congratulations to Levent, thanks to Akhil for suggesting the problem to him, and thanks to DeepMind for already having formalized the statement and thus making formal verification of the counterexample a triviality.
The Jacobian conjecture is resolved! Wow! The next step in that work is for humans to understand exactly what is going on with the example. For the true value of work like this is to give humans better understanding of mathematics. Indeed Akhil has been working on trying to understand the Grothendieck counterexample in a way which is far deeper than “here is a random presentation of a random ring and a random calculation which shows that something doesn’t work”. What we need next is the insight which can be drawn from these extraordinary examples.
What a time to be alive.
You said:
> > nor are they trained for each task individually.
> They are explicitly trained for each task individually.
And that's the main misunderstanding.
Collins says:
individually in American English (ˌɪndəˈvɪdʒuəli, ˌɪndəˈvɪdʒəli) adverb 1. as an individual or individuals rather than as a group; one at a time; separately; singly
Which is precisely what LMs don't do (in contrast to previous "AI" models, which did do that). They are trained on every datapoint at the same time. So long as we agree on that, I think we are saying the same thing :)