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