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