OpenAI, Lean 4로 소수 간격 186 이하 증명 — 단, 세 가지 공리는 미해결

GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186

▲ 50simonpure11 HN 토론

OpenAI가 GitHub에 'PrimeGaps186' 저장소를 공개했습니다. 이 프로젝트는 Lean 4 정리 증명 보조기로 소수 간격의 하극한이 186 이하임을 형식화합니다. 핵심 결과는 40개의 허용 가능한 정수 시프트 집합이 무한히 많은 두 소수를 포함하는 변환을 가진다는 DHL[40,2] 추측에서 파생됩니다. 증명은 Deligne 유형의 Kloosterman 합 추정과 수치 적분 경계에 의존하지만, 이들은 여전히 공리로 남아 있으며 Lean으로 완전히 증명되지 않았습니다. Python 인증서는 수치 계산을 재현하며, Lean 빌드는 오류 없이 통과했습니다.

이 추정들은 인용된 문헌에서 확립되었지만, 이 Lean 개발에서는 아직 증명되지 않은 입력으로 남아 있습니다.
원문 읽기 →HN 토론RSS

HN 토론

11
  1. ks2048

    맥락 - 위키백과 [0]에 따르면, 불과 며칠 전에 누군가 240의 상한에 대한 증명을 게시했습니다 [1].

    [0] https://en.wikipedia.org/wiki/Twin_prime

    [1] https://arxiv.org/abs/2608.31126

  2. dang

    관련 진행 중인 스레드:

    GPT-6 Astra - https://news.ycombinator.com/item?id=49554643

    (거기에서 https://news.ycombinator.com/item?id=49555621도 참조)

  3. quuxplusone

    이 AI가 생성한 횡설수설이 실제로 말하려는 게 뭘까요? 소수 p, q가 무한히 많고 q=p+186이라는 뜻인가요?

    "결과" 아래 첫 번째 방정식은 밀도가 영원히 1/186보다 큰 소수의 무한 수열을 찾았다는 뜻으로 보이는데, 이는 소수 밀도가 어떻게 작동하는지에 대한 제 이해와 맞지 않습니다.

이 날의 다른 글

2026-09-03