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.

Software Engineering feels a little less impacted?

I don't think so - software engineering has already been completely up-ended; we are showing mathematicians what is next for them.

Sure though wrt your point about mystique there is a difference in psychological importance and cultural meaning - maths at the highest level is far more intellectually challenging and even "glamorous" and represents one of the peaks of human achievement. Ironically though if we allow the invention of AI belongs to our (software engineering) field, this is the first time we've matched those peaks.

I agree with you on not missing manual coding, which in some way surprises me - but it's been a long time since I had the passion of my youth for it.

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.