OpenAI、Lean 4で「素数の間隔が最大186」を条件付き形式証明
GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186
OpenAI が公開した PrimeGaps186 リポジトリは、Lean 4 による素数間隔の上限（lim inf ≤ 186）の形式証明と、それを支える数値証明書を提供します。証明は Deligne 型の評価や数値積分の上界など、3つの明示的な公理に依存する条件付きですが、DHL(40,2) から目的の結果を導出しています。Python 製の証明書は数値計算を再現し、検証環境での成功が確認されています。
この Lean 開発では、これらの評価は証明済みの入力ではなく、未証明の入力として仮定されています。
HNでの議論
11- ks2048
文脈 - ウィキペディア[0]によると、ほんの数日前に誰かが240という上限の証明を投稿した[1]。
- dang
関連する進行中のスレッド:
GPT-6 Astra - https://news.ycombinator.com/item?id=49554643
(そちらから https://news.ycombinator.com/item?id=49555621 も参照)
- quuxplusone
このAI生成の意味不明な文は実際には何を言おうとしているのか？ pとqがq=p+186となるような素数の組(p,q)が無限に存在するということか？
「結果」の下の最初の式は、密度が常に1/186より大きい素数の無限列を見つけたと言っているように見えるが、それは私の素数の密度に関する理解とは一致しない。