the OP's point is that if another academic had submitted that paper to a journal with their Lean code, the paper would likely have been rejected by reviewers regardless of the Lean code

it's just holding OpenAI to the same standard as everyone else

> The Lean artifact shows that there is a proof.

how are you sure, if it can't be explained properly?

update: to me this feels like the equiv of dumping an enormous PR that probably has some great stuff in the code but is poorly explained and documented, and expect the maintainer to try to make sense of it and see if it's valid merge