OpenAI начали публиковать теоремы и доказательства, найденные их моделью Astrai. Первый выложенный результат касается классической задачи аналитической теории чисел о разрыве между соседними простыми числами: Astra опустила константу C до 186, и OpenAI выложили формальное доказательство в Leani на GitHub.

Задача формулируется так: существует ли константа C, такая что бесконечно много пар соседних простых чисел отличаются не более чем на C. Конечность такого разрыва была впервые доказана в 2013 году, после чего константу постепенно снижали усилиями математиков — и теперь в этот процесс включилась ИИ-модель.

• OpenAI выложили результаты на GitHub: репозиторий LongGapsBetweenPrimes и репозиторий PrimeGaps186 с формальным доказательством в Lean
• История снижения константы: в 2014 проект Polymath8i Теренса Тао довёл её до 246, затем Джулия Штадльманн подвинула до 240, теперь Astra — до 186
• Не заявлено, что модель нашла оценку полностью автономно
• Результат опирается на три аксиомы, которые известны в литературе, но формально не были доказаны в Lean
• OpenAI также заявляет об улучшении члена в оценке больших разрывов между простыми числами, который не менялся более 80 лет