[mmoskal]

https://github.com/openai/cdc-lean

[nilkn]

Perfect -- that's great to see. The proof strategy in Lean appears essentially identical to the natural language strategy (as much as is reasonably possible). I think this settles it!