ИИ-система стартапа, существующего 4 месяца, решила 9/12 задач в одном из самых сложных в мире экзаменов по математике Putnam (полное название William Lowell Putnam Mathematical Competition) – это ежегодная очень сложная математическая олимпиада для студентов бакалавриата университетов США и Канады. Она считается сложнейшей на этом уровне. Средний результат часто составляет примерно 0–1 балл из 120. В этом году олимпиада проходила на этих выходных. А сегодня никому не известный очень молодой стартап Axiom объявил о том, что их система AxiomProver решила 9/12 задач конкурса (8 из них в течение самого соревнованию, и одну после его окончания). Это очень высокий результат. По прошлогодней шкале это было бы абсолютное первое место среди ~4000 участников + статус Putnam Fellow (топ‑10 за несколько лет). В этом году место пока неизвестно, потому что ранг зависит от общего распределения баллов. Интересно, что модель не просто доказала утверждения на естественном языке, а формализовала их в Lean. То есть каждое решение уже дано в виде машинно-проверяемого proof‑скрипта. Интересно, участвовали ли Google и OpenAI