OpenAI формализовала в Lean 4 доказательство: простые числа-близнецы встречаются бесконечно часто с расстоянием не более 186
GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186
OpenAI опубликовала репозиторий PrimeGaps186, содержащий формализацию на Lean 4 утверждения о том, что существует бесконечно много пар последовательных простых чисел с разницей не более 186. Формализация условна: она опирается на три явные аксиомы, включая оценки сумм Клоостермана, следующие из работ Делиня и других авторов. Также включен численный сертификат на Python, который проверяет вычислительные оценки, но не устраняет аксиомы. Проект использует Lean 4.34.0-rc2 и успешно собирается.
Эти оценки установлены в цитируемой литературе, но остаются непроверенными входами в этой Lean-разработке.
- ks2048
Контекст — согласно Википедии [0], всего несколько дней назад кто-то опубликовал доказательство границы 240 [1].
- quuxplusone
Что эта сгенерированная ИИ абракадабра на самом деле пытается сказать? Что существует бесконечно много пар простых чисел p,q с q=p+186?
Первое уравнение в разделе "Результат", похоже, утверждает, что они нашли бесконечную последовательность простых чисел, плотность которых всегда больше 1/186, что не соответствует моему пониманию того, как работает плотность простых чисел.
- dang
Связанная текущая ветка обсуждения:
GPT-6 Astra - https://news.ycombinator.com/item?id=49554643
(см. также https://news.ycombinator.com/item?id=49555621 оттуда)