← Back to context Comment by JonChesterfield 15 hours ago by fucking sorry written at the end of the proof 4 comments JonChesterfield Reply sebzim4500 14 hours ago 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... mattr03 14 hours ago https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050...looks like the real proof is in this file JonChesterfield 14 hours ago awesome, thanks! ollin 14 hours ago 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...
sebzim4500 14 hours ago 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...
mattr03 14 hours ago https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050...looks like the real proof is in this file JonChesterfield 14 hours ago awesome, thanks!
ollin 14 hours ago 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...
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...
https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050...
looks like the real proof is in this file
awesome, thanks!
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...