The dump from OpenAI seems to be the opposite: huge, messy, and incomprehensible, and taken seriously only because of Lean.

Math papers were hard to comprehend well before AI. This is hardly new. For example, here’s a screenshot of a paper from 40 years ago:

https://i.imgur.com/kPFlczp.png

At least with AI, you can download the LaTeX, upload the paper to your favorite LLM, and have it explain the paper at whatever level of granularity you like. That wasn’t possible even two years ago.