Comment by amelius

Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?