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.
My motivation to do mathematics is some combination of wanting to understand the system of mathematics deeply and enjoying the craft and puzzle of working on research problems. If I never had to publish again and the computer was 1000x better than me, so that I can live on my 20k a year UBI, then I’m fine with that. The anxiety is that this isn’t realistic at all so I’ll likely have to spend my life doing something different than pondering math now.
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.
> While tribe fear hot whispering rock, Wise number shaman wield it. Make cave painting faster, better. No fear. Shaman top mammoth hunter, king hill.
Other tribe not hate whispering rock. Tribe hate rock salesman saying it solve every problem.
Thinking rock make many wrong marks! Shaman must check every mark himself! Whispering rock speak with big confidence even when wrong. Dangerous rock! Who clean mess? Shaman!
Soon shaman forget how to hunt! Today rock help shaman. Tomorrow chief say no need shaman. Me worry.
I don’t see enough people here expressing awareness of the deep societal revolution that is about to unfold. I’m grateful to Terence Tao for doing his best in this strange time to discover how human mathematics can adapt, but I’m not sure why you think this means he’s some uncritical user of AI. And he’s definitely not so shallow as being primarily motivated by staying at “the top”. That’s just silly.
Tao:
“There will be some places where we should use AI, but we should take initiative and decide what those are,” he said. “We set the rules on what’s acceptable or not, and we should not let external actors define those for us.”
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 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.
My motivation to do mathematics is some combination of wanting to understand the system of mathematics deeply and enjoying the craft and puzzle of working on research problems. If I never had to publish again and the computer was 1000x better than me, so that I can live on my 20k a year UBI, then I’m fine with that. The anxiety is that this isn’t realistic at all so I’ll likely have to spend my life doing something different than pondering math now.
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.
> While tribe fear hot whispering rock, Wise number shaman wield it. Make cave painting faster, better. No fear. Shaman top mammoth hunter, king hill.
Other tribe not hate whispering rock. Tribe hate rock salesman saying it solve every problem. Thinking rock make many wrong marks! Shaman must check every mark himself! Whispering rock speak with big confidence even when wrong. Dangerous rock! Who clean mess? Shaman! Soon shaman forget how to hunt! Today rock help shaman. Tomorrow chief say no need shaman. Me worry.
I don’t see enough people here expressing awareness of the deep societal revolution that is about to unfold. I’m grateful to Terence Tao for doing his best in this strange time to discover how human mathematics can adapt, but I’m not sure why you think this means he’s some uncritical user of AI. And he’s definitely not so shallow as being primarily motivated by staying at “the top”. That’s just silly.
Tao: “There will be some places where we should use AI, but we should take initiative and decide what those are,” he said. “We set the rules on what’s acceptable or not, and we should not let external actors define those for us.”
https://www.simonsfoundation.org/2026/08/13/fields-medalist-...
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.