OpenAI, Lean 4로 소수 간격 186 이하 증명 — 단, 세 가지 공리는 미해결
GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186
OpenAI가 GitHub에 'PrimeGaps186' 저장소를 공개했습니다. 이 프로젝트는 Lean 4 정리 증명 보조기로 소수 간격의 하극한이 186 이하임을 형식화합니다. 핵심 결과는 40개의 허용 가능한 정수 시프트 집합이 무한히 많은 두 소수를 포함하는 변환을 가진다는 DHL[40,2] 추측에서 파생됩니다. 증명은 Deligne 유형의 Kloosterman 합 추정과 수치 적분 경계에 의존하지만, 이들은 여전히 공리로 남아 있으며 Lean으로 완전히 증명되지 않았습니다. Python 인증서는 수치 계산을 재현하며, Lean 빌드는 오류 없이 통과했습니다.
이 추정들은 인용된 문헌에서 확립되었지만, 이 Lean 개발에서는 아직 증명되지 않은 입력으로 남아 있습니다.