Доказательства модели OpenAI можно проверять кодом: компания опубликовала формализации Lean

Lean проверяет математическое доказательство, записанное на специальном языке. Для части работ в openai/math доступны такие формализации, а каталог ведёт к PDF, исходникам и инструкциям сборки.

Вместо прежних тестов. OpenAI перешла к открытым исследовательским задачам после того, как модели достигли потолка на прежних математических оценках. За время оценки модели предложили около 4 000 задач. Средний результат потребовал вычислений, эквивалентных примерно 3 часам ChatGPT Pro thinking.

Компания также опубликовала 10 сокращённых изложений рассуждений модели. Среди тем есть приближение числа π дробями и умножение комплексных матриц. Для матриц документация формализации даёт границу ω(C) ≤ 9/4 по числу арифметических операций, а не замер ускорения программы.

Проверка у себя. В репозитории есть инструкция для Comparator, инструмента проверки доказательств. После установки comparator, landrun и lean4export в PATH из каталога lean/ выполняются команды:

```sh lake update lake exe cache get lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json ```

OpenAI рекомендует собирать Lean-библиотеку небольшими частями. При низком vm.max_map_count в Linux сборка целиком может упасть, поэтому в документации предложена сборка Lean с параметром `-DMMAP=OFF`.

Первоисточники: [публикация OpenAI от 6 октября 2026 года](https://openai.com/index/sharing-ai-progress-in-mathematics/), [каталог работ и описание оценки](https://github.com/openai/math), [формализации Lean](https://github.com/openai/math/blob/main/lean/formalization.yaml), [инструкция Comparator](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/README.md).

OpenAI работает над выпуском модели, которая получила эти результаты.