OpenAI опубликовала на GitHub 722 математических результата — теоремы с доказательствами, которые получила её внутренняя топ-модель. Параллельно доступны 10 полных расшифровок цепочек рассуждений, а на каждую задачу в среднем уходило 3 часа в режиме размышления ChatGPT Pro. Lean как язык проверки. Все доказательства формализованы на языке Lean — это не просто записи в блокноте, а верифицируемый код. Математическое сообщество может запустить проверку и убедиться, что модель не нагенерировала правдоподобного, но ошибочного. Что не раскрыто. Неизвестно, идёт ли речь о GPT-5 или о чём-то внутреннем и отдельном. Неясно и главное — новые ли это теоремы или уже известные, просто переведённые на формальный язык. Текст ответа на оба вопроса не даёт. OpenAI заявляет о подготовке к ответственному открытию модели, но когда именно — не уточняет. Что это значит: компания меняет подход к внутренним результатам и впервые делает их доступными для проверки извне, а не для демонстрации в презентациях.