> 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.
This seems to be a common and continuing objection to the OpenAI math repo release. Specifically that at least some, perhaps many of
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.