Comment by vilhelm_s

The OpenAI announcement says

> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.

This seems pretty clear that they found the proof first and then mechanized it afterwards.