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：https://openai.com/index/model-disproves-discrete-geometry-conjecture/ 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：https://logicalintelligence.com/, 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：https://www.claymath.org/events/formalizing-class-field-theory/ 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.
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：https://math.uchicago.edu/~amathew/ 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：https://ems.press/content/serial-article-files/51994 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.
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：https://x.com/__alpoge__/status/2079028340955197566?s=20 that Fable had found a counterexample to the Jacobian Conjecture：https://en.wikipedia.org/wiki/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：https://github.com/google-deepmind/formal-conjectures/pull/4474 to DeepMind’s Formal Conjectures repo：https://github.com/google-deepmind/formal-conjectures. 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.
Thanks for this article. You write that you are “not reading AI-generated informal mathematics” but also that “the next step in that work is for humans to understand exactly what is going on with the example.” How do we do this without reading the informal AI output? We are surely not going through a thousand-line Lean file?
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4839&_wpnonce=611d4e061b Like
I actually find it easier to go through the formal output than the informal output. With the formal output, there is no danger of imagining things or misinterpreting the argument. Most reasonable Lean developments are organized into logical progressions of lemmas, and most of the lemmas might even be obvious to someone well versed in the field (who can also read Lean, of course), leaving only a small amount of actual argumentation to read.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4848&_wpnonce=ef34c24134 Like
Well, that’s because you are versed in Lean. IMO, Lean proofs are very hard to read as a begginner, compared to, say Isabelle/HOL. If human understanding is the main objective “informal output”, which I believe is a Latex document, for example shouldn’t be relegated at all.
It will be very sad if, in the future all proofs are machine-generated in lean/rocq/whatever proof assistant only, and relegating knowledge to the handful of people that know the proof assistant AND are experts in the specific field.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4866&_wpnonce=99a1d09e1c Liked by 1 person：#
I only started using Lean three months ago; I would hardly call myself an expert. Nobody really “reads” Lean in the traditional sense of reading a static artifact. You step through the proof interactively and observe the state transformations at each step.
It takes a fair bit of training to read mathematics in the first place. Reading Lean is only a small difficulty increment on top of that, provided that one is motivated to learn.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4879&_wpnonce=2b36a92851 Like
Parsing through so much LLM and Lean output is exactly the bottleneck I think is coming this year. We’re going to be dealing with two huge issues going forwards
For newcomers to Lean especially, the bigger risk imo is formalizing something different that what they thought they were formalizing.
Both of these are fundamentally a UI/UX problem about how human mathematicians will deal with information overload and it’s exactly what we’re addressing at https://mathvision.ai/：https://mathvision.ai/ 🙂 Check it out for free if you’re interested.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4858&_wpnonce=eaf031ee8e Like
“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.”
With due respect, I find this comment disgusting. Among other problems, this money will be used for the gigantic V-sign to future generations that is building lots of extra gas power plants to supply new data centers. I won’t judge people for doing it any more than for eating red meat, and especially not in such a toughly competitive academic system, but if you think it’s crazy not to give 10% of your salary to unethical companies if it might hurt your career, then we are fundamentally not operating on the same set of values.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4840&_wpnonce=e68045bc2b Liked by 4 people：#
With the caveat that the internet and years of social media encourage us to make kneejerk responses, my instinct is to concur with JAS’s comment/reply. Aside from views one may (or may not) have about the companies building and selling these tools, the sentiment that Kevin candidly admits to is not a mentality that I want to see encouraged among those doing a PhD.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4842&_wpnonce=0e5a0eb3a1 Liked by 1 person：#
There are possibly political or social welfare reasons why one should resist the AI takeover of mathematics. But, from a strict utilitarian standpoint, these tools make you much more than 10% more productive, and are well worth the cost.
I worry about the social implications of handing over a large portion of our resources to AI companies, and the equity and access concerns for people from countries where $200 is a lot of money. Also, there is evidence that AI companies are subsidizing the present cost of subscription access and that the true cost is much higher than what we pay.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4847&_wpnonce=2bea7100ae Like
you should inform your opinion on actual numbers, data centers use a small fraction of electricity and water compared to, say agriculture. so if you’re the kind of person who judges people for eating red meat, you need to dish out that judgement proportionally for AI users.
i’ve given the exact same advice to graduate students months ago, pay for the best models, especially now that they are still affordable. contribute to proving the use case (at this point, is there even any doubt?), and get your department / advisor to pay for the models going forward.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4844&_wpnonce=b7679e2bb6 Like
idk if this is satisfactory but here’s how GPT interpreted the Jacobian example. Take P1xP2->P3 (Union of divisors on P1 say), remove ramification locus and remove a hyperplane of P3 which is tangent to a point of the map P1->P3 (tripling the divisor) but not osculating (multiplicity exactly two). Then the preimage is A3 by direct computation.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4841&_wpnonce=6833b187db Like
On a more constructive note than my previous comment/post: in the hope that some people who follow this blog as part of their interest in/commitment to formalization are also interested in understanding algebraic geometry, I want to give a signal boost to https://sbseminar.wordpress.com/2026/07/20/the-new-counterexample-to-the-jacobian-conjecture/：https://sbseminar.wordpress.com/2026/07/20/the-new-counterexample-to-the-jacobian-conjecture/ so that some maths discussion takes place there.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4843&_wpnonce=7b61124922 Like
A pretty important set of philosophical questions: what is the point of mathematics and the role of mathematicians when the task of formally proving conjectures has been outsourced to a team consisting of a large language model and a proof assistant? What’s the point of mathematical rigour when mathematicians no longer have to develop and write proofs out by hand?
I feel like whatever remains of the formalist viewpoint of mathematics has been largely disproven by developments in the past few years in artificial intelligence and proof assistants: clearly there are still activities for mathematicians in an era where large language models are the ones writing formal proofs in a proof assistant.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4851&_wpnonce=711b4dabd8 Like
“what is the point of mathematics and the role of mathematicians when the task of formally proving conjectures has been outsourced to a team consisting of a large language model and a proof assistant?”
The role of mathematicians is not just to prove conjectures, but also to formulate them. Formulating an interesting/important/useful statement that is a candidate for a theorem often requires as much creative insight (if not more) as does proving it.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4873&_wpnonce=b7139e08dd Like
For now, I agree, it is still true that humans have an edge in formulating conjectures and judging the importance of the results. But I can reasonably imagine a world where machines get better at formulating conjectures.
The next moat behind inquiry and judging is liability and responsibility. I believe there have been a number of court cases where customers interacting with AI customer service chatbots received incorrect information from those chatbots (for example, an airline’s chatbot claiming that a ticket purchase was refundable when it wasn’t). In all of these cases, the companies that those chatbots were supposedly representing were held liable for the statements that the chatbots made (e.g. the company was forced to honor the promised refund). For now, many companies are skittish about allowing their machines to assume liability on their behalf. The human is still the final backstop for liability purposes.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4881&_wpnonce=fa96b95c51 Like
I have one article (with Graber, Harris and Mazur) that disproves a conjecture about rational points that Serre posed in correspondence with Grothendieck. Our theorem proves that a counterexample to the conjecture exists (as a corollary of a more general theorem), but our method gives no explicit counterexample. Almost immediately afterward, somebody sat down and found an explicit counterexample. Honestly, that explicit counterexample could probably have been found (by a dedicated human) anytime in the four decades the conjecture was open, but the community expected the conjecture to be true. If the conjecture is true, it is a waste of resources to search for counterexamples. Now AI means that sort of “checking for counterexamples” can probably be done automatically. That is a fantastic development! As others have said, we could try to *disprove* positive characteristic resolution of singularities (by disproving some of the corollaries about specific congruences of rational points of specific varieties over specific finite fields).
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4884&_wpnonce=1c337d5605 Like
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.
Maybe you intended to express enthusiasm for how good AI has gotten at mathematics. But from the perspective of a PhD student, this comes across as very tone deaf. In many parts of the world (including Europe and many places in the US), PhD students are paid a pittance and are barely making ends meet. Expecting them to fork out 200 USD/month is extremely unreasonable and unrealistic.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4867&_wpnonce=3f1d2ca959 Liked by 1 person：#
I think we’re all hoping for the Harvard approach where the institution pays for access without docking grad student pay to offset the cost.
I don’t think it’s realistic to go back to the good old days. Even if you yourself forswear AI, you can’t stop other people from using it, and those other people are your competition.
Like ：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/?like_comment=4880&_wpnonce=37b71f919c Like
What we need next is the insight which can be drawn from these extraordinary examples.
扫码直达文章详情