Navier-Stokes-Problem offenbar gelöst: OpenAI präsentiert Lean-Beweis

Das Clay Mathematics Institute hat amtlich auf die Ankündigung reagiert, dass das Navier-Stokes-Problem “offenbar gelöst” wurde. Dahinter steht OpenAI: Das Unternehmen veröffentlichte Paper zu “Finite time blowup for Navier–Stokes and Euler equations” und hat die Ergebnisse komplett in Lean 4 mit Mathlib formalisiert.

Was bewiesen wurde

Für jede positive Viskosität zeigt OpenAI zwei Resultate:

• Ganzer Raum R³: Es existieren glatte Anfangsdaten und Kraftfelder, für die keine global glatte Lösung mit gleichmäßig beschränkter kinetischer Energie existiert.
• Periodischer Torus R³/Z³: Auch dort gibt es glatte periodische Anfangsdaten ohne global glatte Lösung.

Das entspricht exakt den Alternativen (C) und (D) der offiziellen Clay-Problembeschreibung - gemeinsam mit einem analogen Blowup-Resultat für die Euler-Gleichungen. Damit wäre eines der sieben Millennium-Probleme (je 1 Million Dollar Preisgeld, ausgeschrieben im Jahr 2000) im Sinne eines Breakdowns entschieden.

Verifizierung statt Peer-Review

Der Beweis ist maschinenverifiziert; ein sogenannter Comparator-Challenge soll belegen, dass genau das richtige Theorem bewiesen wurde - inklusive externer Kernel-Validierung. Das Repo NavierStokesAndEuler auf GitHub enthält Lean 4.34-Formalisierungen samt Anleitung zum unabhängigen Nachrechnen.

Clay: bewusst gemächliches Verfahren

Das Institut teilt zwar “die Aufregung der globalen mathematischen Gemeinschaft”, verweist aber auf seine Regeln: Eine Lösung muss erst in einem referierten Fachjournal von Weltruf erscheinen - und frühestens zwei Jahre danach beginnt überhaupt die Prüfung. OpenAIs Veröffentlichung auf der eigenen Website startet diese Uhr noch nicht mal. Ob der Beweis hält, entscheidet am Ende nicht der Blogpost, sondern die Community.

Original: claymath.org - Navier-Stokes Announcement | GitHub-Repo