▲ 501 points
back
256 comments
When I was in grad school, I had the opportunity to take a course from my adviser in which he discussed his current research and some open questions. It was a relatively accessible subject area and the questions were sometimes easy enough that we could meaningfully contribute.
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.
> 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.
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.
> 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.
This kind of professor/researcher/teacher needs more praise. One of the first engineering courses I took when I started out in higher education was taught by such a person.
Maybe it's just me, but I never felt so welcomed and included during my time in higher education as when that lecturer told a bunch of first-year students "here are some things we haven't figured out which you can help with, let me know if you come up with something". It was inspiring and a great introduction to what's otherwise a rather dull first couple of years of academia.
This is probably part of why machines are doing so well at counterexamples. They have no aesthetic commitment to the conjecture and no embarrassment about producing something ugly
> 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.
For a more extreme (although somewhat inverted) version of this, see Zeeman. He spent years trying to find a knotted sphere in a 5D space. Then realised this was impossible and got a proof for it in a few hours. [1]
[1] https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...
There’s a story in How to Solve It that’s basically the same.
> 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.
He spent an entire weekend before having the wisdom to pause, and let someone else contribute their time to finding a counter.
> The Jacobian Conjecture
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: 庾信平生最萧瑟，暮年诗赋动江关
I was once in a presentation for a math PhD thesis. During the thesis, the evaluator of the thesis noticed a flaw in their proof. The student understood and then asked “What now?” The evaluator prof simply shrugged.
Inspiring? Because of the twin prime conjecture success following his time in the wilderness? I suppose so.
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.
ChatGPT's idiomatic translation of the poem:
Yu Xin’s was a life of utter desolation; in old age, his poems and rhapsodies stirred the riverlands.
That's a good thing. It saves people wasting time trying to prove something they now know to be false, so that they can move on to other things to prove, it's a more fruitful use of humanity's time overall at least in the field of mathematics.
proofs by counterexample are effective but ultimately unsatisfying. they get you to an answer but they don't help help you understand and bend you r mind into seeing how the math works and lead you on to the new set of questions.
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 is also a good thing, because it helps to refine the theorem statement. At least, my humble experience in CS theory research is that I’d try to prove a theorem I want to be true, find a counterexample, refine the statement, and continue.
P.S. It helps that in CS lots of theorems are about either inductive or coinductive definitions.
Yes, especially when the counterexample is formally verified. It converts years of speculative effort into a definite answer almost immediately
Except you can't possibly know that. New insight can arise regardless of whether mathematicians are trying to prove or disprove a statement, and regardless of whether the statement ultimately turns out to be true or false.
Human mathematicians have been being out-counterexampled for at least two decades. The main difference, as I understand, is that (A) we now have a lot more compute to throw at such things, and (B) it is currently trendy to do so. But the sizes of counterexample we're seeing are around about what I'd expect pre-generative-AI counterexample search systems to be able to find.
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.
> about what I'd expect pre-generative-AI counterexample search systems to be able to find.
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.
The word "just" is the mark of a coward.
AI is only as good as a human mathemetician, which we don't have enough of? "just"?
https://en.wikipedia.org/wiki/Jacobian_conjecture
> The conjecture was first stated for two variables by Ludwig Kraus in 1884 [...] an example of a difficult question in algebraic geometry that can be understood using little beyond a knowledge of calculus.
> The Jacobian conjecture is number 16 in Stephen Smale's 1998 list of Mathematical Problems for the Next Century. It was notorious for the large number of published and unpublished false proofs that turned out to contain subtle errors.
> 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.
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.
I suppose it will fall to AI as well to compose the mathematical equivalent of The Ballad of John Henry. Who will be the human champion, the last great hero who can deliver proofs "from the book" that a machine cannot outperform?
BTW, counterexamples in mathematics are really important and often help to refine definitions and sharpen proofs.
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.
I wish I had LLM-built Lean formalisations in university, so much of the math in the slides had errors, and some professors are very bad and ungracious admitting it, while simultaneously rejecting requests for clarifications by saying "the proof is in the slides".
Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.
mathematicians have been using computers for well over half a century, but this was after "bounding" the problem first and then running through the cases with a computer. Now AI is doing the first part. However, mathematicians are still needed at crafting prompts, and knowing where to look, still. The prompt for the Jacobian conjecture was obviously not random. the search space is too big to just try all the combinations of 3 variable polynomials.
If the poster's (is it Kevin Buzzard?) suggestion works out and AI finds a counterexample to the Hodge conjecture, that would be a really big deal. It's one of the Millenium problems, for example.
One thing that he mentions that already quite surprising is that AI was able to autoformalize the Golod-Shaferevich theorem and proof.
How do mathematicians view counter examples? Is it like an unexpected result in the physical sciences: annoying in the moment but potentially stupendously important as it reveals some inaccuracy in the current models? Or is it more like a bug report in coding… probably just, another little annoying detail?
A lot of this math is beyond my comprehension, but it often seems to talk of proofs of theorems. What I want to know is if we continue on this accelerated AI mathematics trajectory, will we eventually be discovering new forms of math that will in turn have some applications down the line in engineering or biomedicine etc? I guess what I’m asking is are we on the cusp of a huge breakthrough for humanity, or largely just proving what was already known?
> 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.
It seems to me also that the very vocal anti-LLM crowd are in the denial phase of grief.
Isn't this exactly what we should expect/hope for?
At least initially, chess computers were better than humans not because they were more creative or inspired, but because they thought harder/deeper. That's exactly the sort of "find counterexamples to this if they exist" work that we're seeing here.
Eventually computer chess got to the point where humans look at some moves and say, "That's an amazing, inspired move. That's not a 'bot' move at all, I can learn from this." We're just not there yet with AI/math in general.
When I was still much more skeptical of AI, I asked ChatGPT to write me a proof of the Goldbach Conjecture. Of course it didn't, but it gave me a several-screens-long research program for how one might get there, with a few alternate paths and what pieces are still missing from each one. Maybe it cribbed that all from some grad student's blog, but it was still pretty impressive.
A week or two ago I asked Claude Code to write a comprehensive testing plan for a new Postgres feature I wrote, UPDATE/DELETE FOR PORTION OF. I was a bit anxious about how many bugs were discovered as soon as it was merged this spring. Claude found some untested areas, then it wrote more tests for them. I'm not talking about LOC covered, but feature combinations. (I've been meaning to submit this as a followup patch. . . .) Fortunately it didn't find any more bugs.
I sense that testing plan has affinity with the findings in the OP, even though it is far more humble than research mathematics. Even better would be if we knew good ways to express invariants about Postgres's behavior, and then we could ask LLMs to violate them. I'm sure there are good ways already, and the "we" who is not knowing is not "all humans" but "the Postgres team" or just "me".
As a counterexample to the article (heh): even though Claude didn't uncover any new bugs, a human did, just a few days ago. Alas!
A missed chance to start with https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...
This will soon happen with theoretical physics, computer science, and everything which can be verified cheaply. Then, we will have long running projects augmented by agents for 2-4 years while AI companies are collecting data of human workflows. After that we will see AI being able to do those projects by themselves. This will lead to super fast human progress and cheap products. The price of things will be bound by energy and natural resources. Interesting times are ahead of us
the AI doesn't even gloat. a rival mathematician would at least title their paper 'a remark on the falsity of...'
I wonder if at some point mathematicians will be over-flooded with proofs to check and eventually some over confident false claim will make it into math.
Maybe in the future the work of Mathematicians will be like the ones of SWEs with AI, check thousands of lines of AI generated proof and find the subtle errors
as someone who loves math, I want to collaborate with mathematicians to solve some hard problems
Next step: "the AI can't find a counterexample, so the conjecture must be true!"
A large fraction of the problems assigned in the Ross Program were of the form "Prove or disprove, and salvage if possible." The rest were usually a calculation, meant to motivate a general proposition you would encounter soon after.
Rest in Peace those of us unable to afford those models.
So before making a claim, see if AI can produce a counterexample that makes sense
Which conjectures will be proven false via counterexample next? Dixmier? Poisson?
Math seem like the most base thing AI will dominate first.
Today I learned a new word...
"Outcounterexampled": there's a neologism worthy of German.
Cal Newport has a grounded take on what the Erdos thing meant in practical terms: https://youtu.be/fhZRWZ6J4k4
Long story short this is much less impressive than it was sold to be. Basically they had mathematicians combing through long winding chains of thought (incidentally: you wouldn't have access to that reasoning) and cleaning it up and making it coherent. That doesn't mean its unimportant, but we're being gaslit about the amount of human steering and human effort that went into this.
A plea: please stop upvoting hype that comes from these labs. It takes time to evaluate their claims and they're always less impressive than claimed.
The framing in these posts is nonsense. ChatGPT isn't doing shit. Human mathematicians using ChatGPT are breaking boundaries.