Sendov's conjecture finally proved for all degrees
A digestion of the proof of Sendov's conjecture
Terry Tao presents a human-readable digestion of an AI-generated proof that resolves Sendov's conjecture for every polynomial degree, along with the stronger Phelps–Rodriguez conjecture. The argument is remarkably elementary, relying only on the fundamental theorem of algebra, Möbius transformations, and a special case of Maclaurin's inequality. A Lean formalization with about 15,000 lines of code verifies the proof, which also yields a new proof of Rubinstein's theorem.
The proof ends up being remarkably elementary. No complex analysis is used other than the fundamental theorem of algebra (and very basic facts about Möbius transformations); and the deepest inequality used as input is the Maclaurin inequality.
- fwlr
Mathematics is like this. You read the first symbol in the paper, it is a wiggly triangle, what does that mean? Well you will find out that symbol means the Constant or Operator or Set or Function belonging to So-and-So with the unfortunate name. Well now you know it is called Grossediche’s Member, what does that mean? You will find out it is defined in these dozen lines in Grossediche’s seminal paper, you will need to read the entire paper to make sense of these dozen lines, you will need to read everything he published in this particular decade to make sense of the paper. Each of the dozen lines is jam packed with other symbols, for each of those you will have to repeat this entire process, with another stack of papers, from another unfortunately named mathematician. Now you have a firm grasp on Grossediche’s Member, you return to the original paper. You read the second symbol in the paper, it is a half-melted letter t, what does that mean? Well, …
Behind each symbol is a whole paper, behind each paper is a whole life’s work, and so on. With this in mind, it is perhaps not so surprising that language models operating on embeddings are extraordinarily well-suited to this particular task.
- glimshe
While so many are complaining about AI on HN, an absolute master of his field is using it without any self-doubt or negativity. Just getting stuff done better and faster while remaining at the top.
- brotchie
The impact on the psyche on some Mathematicians of this AI progress must be pretty brutal. To me, it breaks the mystique of Mathematics a lot.
You still need a lot of skill to digest and understand the proofs, but "this is the worse it will ever be." I'd imagine part of the motivation of a large set of mathematicians is to be the "first" or to crack the nut that others couldn't. If Mathematics becomes working with an AI to get a Lean certificate, and then essentially reverse engineering that into something digestible, then it's fundamentally a different pursuit.
Software Engineering feels a little less impacted? Though if you identify with loving coding, then perhaps similarly? I've always liked the outcome of what writing code can do, and enjoyed the craft hand coding for the past ~30 years. But I haven't once ever missed writing code by hand since Opus 4.6, I couldn't go back.
- PowerElectronix
Just like in chess, at some point the problem at hand and its solution becomes so unwieldidly complex that you either make of it the work of your life or you use a math/chess engine to handle the complex stuff.
Just like you can find a forced mate in 120 moves for a given position, you can find a 120 pages of pure gibberish demonstration of some conjecture with its lean check.
The thing is to not become reliant on it and just cheer it up so it makes progress on its own in the Riemann hypothesis, but to use it like a lever to lift heavier stuff, as Dr. Tao does here.
- msteffen
I saw an interesting article in the Atlantic[^1] somewhat recently predicting that the people who will thrive in the AI age will be ones who enjoy mental effort. That is, even when AI could do something for them, these people will choose to do it themselves if there’s something to be learned from it.
This post seems to illustrate the point perfectly to me. AI wrote the proof. It was done, Lean checked it. And presented with that, Tao’s reaction is still to want to learn something—how to solve the problem himself—and then to meticulously untangle a 90k-line machine proof (utterly disregarding that there’s no clear upside for doing so—he can’t get a paper out of this) because it’s the only way to learn that. My bet is that it was worth it.
(I also think everyone saying “it doesn’t make sense to write code anymore” is crazy. The best learning tool of all time was just invented, and you want me to not use it? What the point of any of us if not to know things?)
[^1]: https://www.theatlantic.com/ideas/2026/06/ai-open-ai-anthrop...