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.