> the more raw these proofs are, the better

There are parts of mathematics where the result is the important part. That's not what we're seeing here. Knowing whether the partition principle implies the axiom of choice doesn't meaningfully shape downstream knowledge and decisions. For these more foundational problems, clever proof techniques and the exposition around them are literally the point. Without that, neither humans nor AI can take this slop and derive anything useful.

And if AI can do that then great. I don't care about being elitist or not, and I'm fine with AI taking over math. That's not what it's done though, at least not yet.