Daniel Kokotajlo comments on OpenAI Solves (Some) Formal Math Olympiad Problems