Lean 4'te koşullu bir formalizasyon, aralarındaki farkın en fazla 186 olduğu asal boşluklarını iddia ediyor

Yayınlanan şey ne

OpenAI'nin GitHub hesabı altında yayınlanan ve Hacker News ana sayfasına taşınan PrimeGaps186 adlı depo, bir asal boşluğu sonucunun Lean 4 formalizasyonunu ve sayısal çalışmayı yeniden doğrulayan bir Python programını içeriyor. Ana sonuç, ardışık asal boşluklarının p(n+1) − p(n) limit inferiorunun en fazla 186 olduğu — yani basit bir deyişle, sonsuz sayıda komşu asal çiftinin 186 veya daha az farkla ayrıldığı. README, projenin durumu konusunda açık sözlü: Lean sonuçları açıkça bildirilen üç girdi aksiyomuna koşulludur ve bu aksiyomların kodladığı analitik tahminler ile sayısal hesaplamalar henüz Lean ispatlarına dönüştürülmemiştir.

Matematiksel yol

Formalizasyon, sayı teorisyenlerinin DHL[40,2] dediği sonucu türetiyor: kırk tam sayı kaydırmdan oluşan her admissible kümesi, üyelerinden en az ikisinin asal olduğu sonsuz sayıda öteleme kabul eder. Buradaki admissible olma, her asal için kümenin o asala göre modüler tüm artık sınıflarını kaplamaması anlamına gelir. Depo, çapı 186 olan açık bir admissible tuple ile geliyor — en küçük ve en büyük elemanları 186 arayla yer alıyor — ve bu tuple'a DHL[40,2] uygulanmak boşluk sınırını veriyor, çünkü genişliği 186 olan bir pencere içindeki iki asal, ardışık bir boşluğun pencereden daha geniş olamayacağını zorunlu kılıyor. Üç ana teorem, PrimeGap186 ad alanı altındaki PrimeGaps186.lean dosyasında yer alıyor: dhl_40_2, infinite_two_prime_translates_admissibleTuple ve primeGapLiminf_le_186.

Varsayılan üç girdi

Koşullu kısım üç aksiyomda yatıyor. İlki olan kloosterman3_bound, normalize edilmiş bir hyper-Kloosterman toplamı Kl3(c;p)'nin mutlak değerce, her asal p ve sıfırdan farklı c için 3 ile sınırlı olduğunu savunuyor. README'ye göre bu, Nicholas Katz'ın 1988 tarihli Gauss Sums, Kloosterman Sums, and Monodromy Groups kitabında belirtilen biçimiyle Deligne teoreminden (Teorem 4.1.1(1)–(2), sayfa 49) kaynaklanıyor; burada rank üç ve ağırlık iki, normalizasyon p'ye bölmeden önce 3p'lik ham bir sınır veriyor.

İkincisi olan kloosterman2_correlation_bound, klasik Kloosterman toplamlarının bir korelasyonunu, tüm asal p'ler ve sıfırdan farklı A ve B parametreleri için 8p·√p ile sınırlıyor; A, B'ye eşit olsa bile iki kutup terimi hariç tutuluyor. Atıf, 14 Haziran 2013 tarihli, Étienne Fouvry, Emmanuel Kowalski ve Philippe Michel imzalı "The Friedlander–Iwaniec character sum" makalesinin 2. Önermesi'dir; README, toplam değişkeni ters çevrildiğinde normalizasyonlarının √p kadar farklılaştığını açıklıyor.

Üçüncüsü olan physical_integral_bounds, sayısal hesapları paketliyor: 104 dış ve 45 iç fiziksel integral üst sınırı ile üç tavan sınırı. README'ye göre ilk iki tahmin atıf yapılan literatürde ortaya konmuştur, ancak üçü de bu Lean geliştirmesi içinde henüz ispatlanmamış girdiler olarak kalmaktadır.

Sayısal sertifika

prime_gap_186_certificate.py adlı sertifika, saklanan değerleri yeniden oynatmak yerine denemeyi sıfırdan yeniden hesaplıyor. Test edilen ortamda Python 3.12.13, NumPy 2.2.6, python-flint 0.9.0 ve düzeltilmiş işaretli polinom konvolüsyonuna sahip özel bir FLINT 3.6.0 derlemesi kullanıldı; proje, bunun pakete dahil edilmediğini belirtiyor. Bir çalışma, zorunlu kayan nokta ve işaretli konvolüsyon kontrollerini geçmek zorunda ve "passed": true işaretli bir makbuz üretiyor. Kritik nokta şu: Makruz hiçbir Lean aksiyomunu ortadan kaldırmıyor — sertifika ve çekirdek tarafından doğrulanan ispat ayrı yapıtlar olarak kalıyor.

Yeniden derleme ve doğrulama

Proje, Mathlib bağımlılıklarıyla birlikte Lean 4.34.0-rc2 sürümünü sabitliyor; elan kuruluysa lake exe cache get ve ardından lake build PrimeGaps186 derlemeyi yeniden üretiyor; geliştiriciler derlemenin hata veya uyarı olmadan geçtiğini bildiriyor. Bir karşılaştırıcı, üç sonucu da — teoremleri ve girdi varsayımlarını üç kasıtlı teorem yer tutucusuyla bildiren Challenge.lean dosyasıyla — eşleştirdi ve hem Nanoda hem de Lean'in çekirdeği ispatları yerel bir Colima Linux sanal makinesinde kabul etti. Aksiyom yapılandırması tam olarak altı aksiyoma izin veriyor — üç proje girdisi artı Lean'in standart propext, Quot.sound ve Classical.choice aksiyomları — dolayısıyla makine doğrulaması koşullu ispatları kapsıyor, girdilerin kendisini değil. Proje katkıları Apache 2.0 lisanslıdır.

Neden önemli

Asallar arasındaki sınırlı boşluklar, 2013'te Yitang Zhang'ın çığır açan çalışması ve onu izleyen Maynard–Tao iyileştirmeleriyle bir teorem haline geldi; Polymath işbirliği koşulsuz sınırı 246'ya kadar indirdi. Tamamen ispatlanmış bir 186 sınırı bu rekoru daha da aşağı çekerdi, ancak bu depo böyle bir iddiada bulunmuyor ve kendi muhasebesi kalan mesafenin tam olarak nerede yattığını gösteriyor.

Projenin gösterdiği şey bir doğrulama mimarisi. Adlandırılmış analitik girdilerden ana sonuca giden tüm zincir, kısa ve açık bir aksiyom listesi dışında makine tarafından doğrulanıyor ve sayısal bileşen, sabitlenmiş ortamlarla ve zorunlu tutarlılık kontrolleriyle bağımsız olarak yeniden çalıştırılabilir bir program olarak geliyor. Bu desen — kesin ifadeler, bildirilmiş varsayımlar, yeniden üretilebilir sertifikalar — hesaplamalı matematik ve otomatik araçlarla üretilen ispat yapıtları için işleyebilir bir güven modeli. Şüpheci bir okuyucu Lean projesini yeniden derleyebilir, sertifikayı yeniden çalıştırabilir ve hangi lemmaların hâlâ açık olduğunu tam olarak görebilir: Kloosterman tahminleri ve integral sınırları. Atıf yapılan literatürü ve sayısal hesaplamaları Lean ispatlarına dönüştürmek bariz bir sonraki kilometre taşı ve bu gerçekleşene kadar 186 sayısı koşullu kalmaya devam ediyor.