Comment by jboggan
11 hours ago
Ah, cool. I'm still learning Lean - is there somewhere else in the repo with the Lean specification of the cycle construction for the full argument?
11 hours ago
Ah, cool. I'm still learning Lean - is there somewhere else in the repo with the Lean specification of the cycle construction for the full argument?
the json file next to the problem statement in lean says the solution starts here: https://github.com/openai/math/blob/main/lean/OAI/Combinator...
the proof is probably split over the constructions in the whole directory.