Модель Astra от OpenAI улучшила верхнюю границу разрыва между простыми числами, опустив константу C с 240 до 186, и предоставила формальное математическое доказательство на языке Lean. Речь идет о фундаментальной задаче аналитической теории чисел: поиске минимального гарантированного расстояния между бесконечным числом пар соседних простых чисел. Исторически планку в 246 единиц установил проект Polymath8 под руководством Теренса Тао еще в 2014 году, а недавняя работа Джулии Штадльманн довела ее до 240. Параллельно OpenAI заявила об оптимизации члена в оценке больших разрывов между простыми числами, державшейся без изменений более восьмидесяти лет.
Впрочем, списывать математиков со счетов рано: речь не идет о полностью автономном научном открытии с нуля. Доказательство Astra опирается на три заимствованные из научной литературы аксиомы, которые пока не верифицированы внутри самой среды Lean. Тем не менее прецедент важен методологически: reasoning-модели перестают быть генераторами правдоподобных текстов и начинают решать содержательные задачи фундаментальной науки в жестко верифицируемых средах.
Для бизнеса этот академический кейс несет прямой прикладной сигнал: переход от вероятностной генерации кода и ответов к проверяемым цепочкам рассуждений в формальных системах наконец открывает путь к внедрению ИИ в критическую инфраструктуру, финтех и контуры с нулевой толерантностью к галлюцинациям.