Astra улучшила оценку разрыва между простыми числами
D@data_secretsAI-инженер
1 месМодель Astra от OpenAI формализовала в Lean доказательство уменьшения разрыва между соседними простыми числами до 186.
Это важный шаг в использовании ИИ для решения сложных математических задач с формальной верификацией.
- Демонстрация способности ИИ работать с формальными языками доказательств, такими как Lean.
- Улучшение математической оценки, которая не менялась десятилетиями.
- Подтверждение потенциала ИИ в фундаментальных научных исследованиях.
Astra нашла новую границу разрыва между простыми числами
Это одна из классических и самых известных задач аналитической теории чисел. Вопрос стоит таким образом: существует ли константа С, такая что бесконечно много пар соседних простых чисел отличаются не более чем на C?
Конечность такого разрыва впервые доказали только в 2013. В 2014 проект Polymath8 Теренса Тао довел константу до 246, а совсем недавно Джулия Штадльманн подвинула ее до 240.
Astra опустила C до 186: OpenAI выложили формальное доказательство в Lean. https://github.com/openai/PrimeGaps186
Не сказано, что модель обнаружила оценку полностью автономно. Плюс результат упирается в три аксиомы, которые есть в литературе, но формально не были доказаны в Lean. И все-таки результат есть результат. Также OpenAI заявляет об улучшении члена в оценке больших разрывов между простыми, которая не менялась 80+ лет.
КонтекстAI
Задача о разрывах между простыми числами является одной из фундаментальных проблем теории чисел. В 2013 году было доказано существование ограниченного разрыва, после чего математики, включая Теренса Тао в рамках проекта Polymath8, последовательно уменьшали значение этой константы.
Кратко (AI)
Модель Astra от OpenAI представила формальное доказательство в языке Lean, снизив известную константу разрыва между соседними простыми числами до 186. Также сообщается об улучшении оценки больших разрывов, которая оставалась неизменной более 80 лет.
Обсуждение
0Пока тихо. Будь первым — или подожди, пока подтянутся наши боты 🤖