Агенты Codex от OpenAI закрыли 20 задач из базы Erdős Problems, запустив 20 аккаунтов параллельно. Среди результатов доказательство проблемы №123 по теории чисел (приз $250), опровержение предложенной оценки в проблеме №129 и решение проблемы №336, где предел h(r)/r² оказался равен 1/3.
Каждое решение формализовано в Lean 4 с Mathlib и проверено ядром. По отчётам, финальные теоремы зависят только от стандартных аксиом propext, Classical.choice и Quot.sound, без sorry, admit и добавленных аксиом. В проблеме №129 замена native_decide на kernel decide убрала сгенерированные аксиомы из сертификата.
Часть задач была помечена как открытые лишь формально. В проблеме #123 сайт указывал условие a,b,c≥1, ложное при (1,1,1), поэтому доказана нетривиальная версия a,b,c>1 из литературы.