OpenAI formalisiert in Lean 4: Unendlich viele Primzahlpaare mit Abstand höchstens 186
GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186
OpenAI hat ein Lean-4-Projekt veröffentlicht, das eine bedingte Formalisierung einer oberen Schranke für Primzahllücken enthält. Die zentrale Aussage: Für unendlich viele aufeinanderfolgende Primzahlen ist der Abstand höchstens 186. Der Beweis stützt sich auf zwei explizite Axiome, die auf Deligne-Typ-Schätzungen für Kloosterman-Summen beruhen, sowie auf numerische Zertifikate. Die Formalisierung ist konditional – die mathematischen Eingaben sind nicht in Lean bewiesen. Das Repository enthält den Lean-Code, ein Python-Zertifikat und Anweisungen zum Bauen und Verifizieren.
Die Lean-Ergebnisse bleiben konditional bezüglich dreier expliziter Eingabe-Axiome; die zitierten mathematischen Abschätzungen und numerischen Berechnungen wurden nicht in Lean-Beweise dieser Eingaben umgewandelt.
- ks2048
Kontext - laut Wikipedia [0] hat vor ein paar Tagen jemand einen Beweis für eine Schranke von 240 veröffentlicht [1].
- dang
Zusammenhängender laufender Thread:
GPT-6 Astra - https://news.ycombinator.com/item?id=49554643
(siehe auch https://news.ycombinator.com/item?id=49555621 von dort)
- quuxplusone
Was will dieses KI-generierte Kauderwelsch eigentlich sagen? Dass es unendlich viele Primzahlpaare p,q mit q=p+186 gibt?
Die erste Gleichung unter "Das Ergebnis" scheint zu besagen, dass sie eine unendliche Folge von Primzahlen gefunden haben, deren Dichte für immer größer als 1/186 ist, was nicht mit meinem Verständnis davon übereinstimmt, wie die Primzahldichte funktioniert.