They do that to make it easier for readers to verify the statement (which is entirely contained in that file) separately from the proof (which is spread over thousands of files and github can't even show them all).

Proof is at https://github.com/openai/math/tree/main/lean/OAI/Algorithms...

I was confused too, but it looks like https://github.com/openai/math/blob/main/lean/ComparatorChal... (with the sorry at the end) is just the problem statement; the actual proof is a big pile of lean in the Algorithms folder, with the final theorem stated here https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050...