A digestion of the proof of Sendov's conjecture

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.

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.

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.

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.

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...

Making things understandable is part of intelligence as much as producing the initial artifact is. Even if the proof checks out in Lean (or the code runs and passes QA) if it's a mess, it will be hard to use it to do anything further.

This does not only matter doing cutting-edge mathematics. This, about the 'digested' version versus the original, should feel familiar to some folks here:

> This formalization is more streamlined than the original formalization (it has about 15,000 lines of code, compared with around 90,000 for the original proof).

and if you've ever tried to turn an overly vibed piece of code into something that makes sense:

> it has taken me several days (with heavy AI assistance) to perform such a digestion, to place the proof in proper context with previous literature and to simplify and streamline the argument to highlight the main ideas

If you see something that is confusing or overly clever, please don't assume it must be for some good reason you don't understand and move on--ask questions, get it simplified, try to get it worked out. Future you will appreciate it.

"The proof ends up being remarkably elementary."

Dude then proceeds to dump about 16 A4 pages worth of heavy-duty algebra which 99.999% of the humans on the surface of this planet are completely unable to read past the first two lines.

LOL, I guess language is a "remarkably" vague tool, where "elementary" means vastly different things to different people.

That doesn't diminish the achievement of course, but ... please, easy on the "remarkably elementary" next time, that's borderline insulting.