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.

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.