Comment by remus

While I think there is some truth to this I think the framing is very uncharitable. The obscurity in maths comes from layers upon layers of abstraction because this is a useful way for humans to work with these complex ideas. I think we see some of this with these proofs that have been translated to lean: some of the proofs are millions of lines of lean, imagine trying to wrap your head around a codebase that is millions of lines! And just for a single proof! These impenetrable abstractions that mathematicians have created are like a mental model for a massive code base.