Some of the lean proofs are apparently incomprehensible.

It would be like trying to look at a completed video game's assembly code, being told that it was call of duty, and then being asked questions about the high level code architecture.

AI models are perhaps unsurprisingly good at low level translation (see the progress being made for decomp games)

These models have surpassed human capabilities at math/machine code, but they can't "simplify" yet - in part because they don't have the same need to due to their comparative lack of cognitive constraints. AI Slop code is getting better, but it takes time. At the moment, its embarrassing frankly. It will come eventually, but right now OpenAI is not handling this with the care, respect, or concern that it deserves.