> For those hard theorems where we really want LLMs to help us, these Lean proofs are extremely long, like hundreds of thousands of lines of code long. A seemingly emergent trend is that the longer the Lean version of a proof, the messier and less faithful its machine-generated “natural language” translation seems to be.

This seems to be a common and continuing objection to the OpenAI math repo release. Specifically that at least some, perhaps many of

  * the natural language proofs are low quality or otherwise extremely difficult to understand (although possibly correct?)
  * the lean proofs are too long, convoluted, or otherwise extremely difficult to understand

I wonder if LLMs will be able to generate "high quality" natural language and lean proofs soon.

And specifically: iterate on the OpenAI repo to produce "better" proofs that prove the same things.