gwern comments on OpenAI Solves (Some) Formal Math Olympiad Problems