jan ahb comments on OpenAI Solves (Some) Formal Math Olympiad Problems