They are using a Lean tool where you separately state your theorems with `sorry` and then prove them elsewhere. The tool checks that all sorry's are covered. This is so the AI doesn't need to edit the specification of the theorem statement.
replyAh, 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?
replythe json file next to the problem statement in lean says the solution starts here: https://github.com/openai/math/blob/main/lean/OAI/Combinator...
replythe proof is probably split over the constructions in the whole directory.