alt Hacker NewsThis is the key bit.
> But, back to the Partition Principle. I took a brief look at the preprint released by OpenAI (not at the Lean code, since I know very little of the actual usage of Lean, and that code was enormous). It sucked. It is unclear, muddled, and has a strange structure.
Incredible lack of curiosity. The Lean artifact shows that there is a proof. Maybe the natural language writeup sucks (maybe it doesn't even correspond to the Lean proof!) but the proof is there and if he were really interested in the problem he would try to understand it. Rather, his revealed preference is that what he's really interested in is good style in academic papers.
Replies
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
>>Incredible lack of curiosity
Maybe on your end because that's the exact point the author explained - these companies need to adhere to the scientific community rather than expecting the opposite.
If the write up - the natural language part - sucks - why are you expecting humans to waste their time on understanding the proof???