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 и успешно собирается.