Das Riemann-Projekt, September 2026 — Ein ehrlicher Statusbericht | Research

Das Riemann-Projekt, September 2026 — Ein ehrlicher Statusbericht | Research | Tobias Weiss

Worum es in diesem Projekt geht

Ein mehrgleisiges Forschungsvorhaben, das die Riemann-Hypothese (RH) von der computergestützten und maschinell verifizierten Seite angreift. Die verbindende Idee ist die Kette

Cayley-Graphen-Eigenwerte → Hecke-Eigenwerte → L-Funktionen → ζ(s)

und das Projekt verfolgt sie entlang vier paralleler Tracks:

GNN-Experimente auf arithmetischen Graphen (Cayley-Graphen von SL(2,𝔽_p), Farey-Graphen, Pizer-Graphen) — mit überwiegend negativen, aber wissenschaftlich wertvollen Ergebnissen.
Datengesteuertes ML auf LMFDB-Daten — der erfolgreichste Track, mit einem veröffentlichten Paper und drei neuen empirischen Befunden.
Statistik der L-Funktions-Nullstellen — eine Studie über 63.844 Formen, die bereits mit DOI auf Zenodo archiviert ist.
Eine Lean-4-Formalisierung eines Transferoperator-Zugangs zur RH — die aktuelle Forschungsfront des Projekts.

Ein Neo4j-Wissensgraph (194 Knoten, 161 Beziehungen, 28 RH-Äquivalenzen) modelliert die theoretische Kette, ein Literaturkorpus mit 3.460 Papern ist in literature/ kuratiert, und eine interaktive three.js-Visualisierung ist auf GitHub Pages veröffentlicht.

Track 1 — GNNs auf arithmetischen Graphen: überwiegend negativ, und das ist die Erkenntnis

Sieben Experiment-Tracks fragten, ob GNNs spektrale oder zahlentheoretische Invarianten allein aus der Graphstruktur vorhersagen können. Die Antwort ist konsistent: GNNs lernen innerhalb ihrer Trainingsverteilung, scheitern aber an der Generalisierung über Primzahlen hinweg.

Track	Graph	Zielgröße	Baseline-R²	GNN-R²	Urteil
1	Cayley SL(2,𝔽_p), Teilgraphen	Spektrallücke	—	< 0	gescheitert
2	Cayley SL(2,𝔽_p), Vollgraph	Spektrallücke	0,782	0,824	marginal
3	Farey-Graph	Spektrallücke	0,9999	−7,57	trivial
4	Cayley, 1 Erzeuger	Hecke-Eigenwerte	0,41	−0,21	gescheitert
5	Cayley, 10 Erzeuger	Hecke-Eigenwerte	0,977	−0,32	gescheitert
6	Cayley, 10 Erzeuger	Spektrallücke	0,43	−2,12	gescheitert
7	Pizer-Graphen (Hecke T₂)	T₃-Eigenwerte	0,057	0,000	keine Generalisierung

Die Fehlschläge sind mathematisch erklärt, nicht durch Tuning behebbar:

Cayley-Graphen sind knotentransitiv. Jeder Knoten sieht exakt dieselbe lokale Struktur (Grad 4, gleiche Clusterung), daher tragen lokale Nachbarschaften keinerlei Information über globale spektrale Eigenschaften. Jeder teilgraphbasierte Ansatz ist prinzipiell zum Scheitern verurteilt.
Die Spektrallücke des Farey-Graphen folgt einem perfekten Potenzgesetz gap ≈ 2,65/n^(0,999); eine log-log-lineare Baseline erreicht R² = 0,9999 (0,07 % Medianfehler). Kein Modell kann ein geschlossenes Gesetz sinnvoll schlagen.
Der einzige Teilerfolg — Vollgraph-ChebConv mit Random Positional Encoding, R² = 0,824 gegenüber 0,782 Baseline — ist real (relativer Vorhersagefehler meist unter 8 % für p ≥ 37, bestes Ergebnis 0,3 % bei p = 37 — mit verrauschten Ausreißern wie p = 31 mit 18,7 %), doch das ΔR² von +0,042 über dem log(N)-Trend trägt kein zahlentheoretisches Signal.

Im Projekt festgehaltene Lehre: Die unterscheidenden Parameter einer Graphfamilie sind global (Größe, Erzeugermenge), und gelernte „Erklärungen" aus lokaler Struktur sind nicht arithmetisch. Es dürfte sich um die ersten systematischen Negativergebnisse an der Schnittstelle GNN × Zahlentheorie handeln.

Track 2 — ML auf 200.000 Newforms: die produktive Wende

Nach dem Scheitern der Cayley-Ansätze wechselte das Projekt zur Datenskalierung: 200.000 Gewicht-2-Newforms aus der LMFDB, jeweils 100 Hecke-Spurkoeffizienten. Dieser Track lieferte die stärksten Ergebnisse des Projekts (siehe auch das Comprehensive Modular Forms Paper):

Analytischer Rang, Klassifikation: F1 = 0,970
Dimensions-Regression: R² = 0,990
CM-Formen-Erkennung: F1 = 0,919 (das M₄/M₂-Momentenverhältnis ist das trennstärkste Merkmal)
Vorhersage der ersten L-Funktions-Nullstelle über eine Trace-Index-Graph-Konstruktion (Newforms, verbunden über gemeinsame Eigenstruktur): ein ChebConv-GNN erreicht R² = 0,631, eine Architektursuche findet GATConv mit R² = 0,731 (+15,9 % gegenüber dem ChebConv-Ergebnis).

Nach der Korrektur eines Normalisierungsfehlers in der Sato-Tate-Momenten- Analyse ergaben sich drei neue empirische Befunde:

Galois-Korrelationskonstante ρ₂ = −0,607 ± 0,012 — eine Antikorrelation zwischen konjugierten Hecke-Eigenwerten bei Dimension-2-nicht-CM-Formen, mit einem Verdünnungsgesetz ρ_d ~ d^(−1,29).
Dimensions-Skalierungsgesetz M₂(d)·d → 0,177 + O(1/d) — eine direkte empirische Sonde der Sato-Tate-Gruppenstruktur über Hecke-Körpergrade hinweg.
CM-Klassifikator F1 = 0,919 (wie oben).

Track 3 — L-Funktions-Nullstellen: der Dimensions-Split

Die statistische Studie, archiviert auf Zenodo (DOI 10.5281/zenodo.21974748), analysiert 63.844 Gewicht-2-Newforms (568.708 Nächstnachbar-Abstände der Nullstellen), passt die Brody-Verteilung β pro Form an und stratifiziert nach Hecke-Körperdimension:

Gruppe	β (MLE)	Interpretation
Alle Formen, aggregiert	0,620	„intermediär" — irreführend
dim = 1 (CM)	1,879	GUE-artig (KS-Abstand 0,017)
dim ≥ 2 (nicht-CM)	0,242	fast-Poisson
Rang 0 / Rang 1	0,676 / 0,538	intermediär

Die Kernaussage: die aggregierte „intermediäre" Repulsion ist ein Artefakt der Vermischung. CM-Formen (~15 % der Population) sind im Wesentlichen GUE; nicht-CM-Formen (~85 %) zeigen eine dramatisch abgeschwächte — fast-Poisson — Level-Repulsion. Eine Tiefenanalyse bestätigte, dass die 1.748 „GUE-Ausreißer" unter dim ≥ 2 genuin repulsiv sind (gepooltes Brody-β) und dass die CM-Eigenschaft nur 1,1 % von ihnen erklärt (3,58-fache Anreicherung, aber 102 Formen) — Level und Wurzelzahl sind wichtiger. Das widerspricht dem Allgemeinplatz, dass alle L-Funktions-Nullstellen gegen denselben Zufallsmatrizen-Grenzwert konvergieren. Details in Der Dimensions-Split in den Statistiken der L-Funktions-Nullstellen.

Interaktive Versionen dieser Befunde (ζ-Landschaft, kritische Linie, Brody-Wasserfall durch den Phasenübergang) sind unter tobias-weiss-ai-xr.github.io/riemann/ live.

Track 4 — Lean-4-Formalisierung: wo das Projekt heute tatsächlich lebt

Die aktuelle Forschungsfront ist eine maschinell verifizierte Formalisierung des Transferoperator-Zugangs zur RH in Lean 4 / Mathlib, 38 Module unter lean/Riemann/. Die ehrliche Bilanz wird in research/FRONTIER.md und lean/Riemann/AxiomAudit.lean geführt — jede tragende Deklaration trägt ein #print axioms-Abhängigkeitszertifikat.

Was wirklich, axiomrein bewiesen ist

All das Folgende hängt nur von den Standard-Axiomen [propext, Classical.choice, Quot.sound] ab:

Der Gauss-Abbildungs- / Ruelle-Transferoperator L_s auf C([0,1], ℂ) ist ein beschränkter Operator mit expliziter Konstante ‖L_s‖ ≤ Σ (n+1)^(−2·Re s) = ζ(2·Re s), samt vollständigem Summierbarkeits-Fundament.
Gleichmäßige Konvergenz der Partialsummen — plus der ehrlichen Korrektur, dass Kompaktheit auf C([0,1]) falsch ist (der n = 0-Zweig verletzt die Gleichgradigkeit; Kompaktheit gehört auf eine analytische Klasse wie die Diskalgebra).
Nichtverschwinden im Euler-Bereich und für Re s ≥ 1 von ζ (trivial-klassisch, aus Mathlib geerbt), Ausschluss der trivialen Nullstellen über die Funktionalgleichung und die Funktionalgleichungs-Reflexion ζ(ρ) = 0, 0 < Re ρ < 1 ⇒ ζ(1−ρ) = 0.
Krein-Rutman in voller Stärke (RH-39): nachdem zwei zugestandene falsche Lemmata mit formalen Gegenbeispielen entdeckt und entfernt wurden (ein Kollaps-Lemma; eine reale Gelfand-Oberschranke, widerlegt durch Complex.I), sind die schwache und die starke Form unbedingt bewiesen — die letzte Lücke wurde durch ein direktes Resolventen-Explosionsargument geschlossen, das die gesamte β-Stabilisierungsmaschinerie überflüssig machte.
Reale Gelfand-Formel für positive Operatoren (RH-38, sorry-frei) — die Oberschranke, die das Resolventen-Positivitäts-Endspiel freischaltet.
Mayer-Halbkreis-Algebra, Phase 2 (RH-40/41/42): die Diskalgebra und die Halbkreis-Algebra als vollständige Unteralgebren stetiger Funktionen (Weierstraß-Abgeschlossenheit bewiesen), die Mayer-Transfersummanden mit ‖T_n‖ ≤ 1/(n+1)² und die kompakte Tail-Architektur — alles gate-sauber, 0 sorries.

Die exakte Front: ein sorry, äquivalent zur RH

Das Repository trägt genau ein offenes sorry an lean/Riemann/TransferOperator/Complete.lean:152:

theorem no_zeros_right_half_plane (ρ : ℂ) (hρ : riemannZeta ρ = 0)
    (hRe : 1 / 2 < ρ.re ∧ ρ.re < 1) : False := by sorry

Diese Aussage — keine Nullstelle im Streifen 1/2 < Re ρ < 1 — ist äquivalent zum schweren Teil der RH (die FE-Reflexion macht daraus die volle Aussage über den kritischen Streifen). Alles andere, was weiter unten wie ein „Beweis" der RH aussieht, ist ehrlich etikettiert:

fredholmDet ist ein definitionales Modell — per Definition ζ(2s)/C(s), nicht det(1−L_s). „Mayers Identität" gilt per Unfolding, nicht per Spektraltheorie.
modelLeadingEigenvalue = exp(1/2 − s) ist ein Modell, gewählt, damit die gewünschten Einheitskreis-Ungleichungen per Analysis gelten; es ist nicht das Spektrum von L_s.

Der ehrliche Weg zur Schließung der Front: (1) Mayers analytische Klasse — in Phase 1–2 erledigt; (2) eine echte Fredholm-Determinante der Spurenklasse und Mayers Identität dafür; (3) Krein-Rutman/ρ(L_s) < 1 bis hinab zu Re s > 1/4 — jeder Schritt ist exakt so schwer wie die entsprechende Hälfte der RH. Kein kostenloses Mittagessen, und die projekteigenen Dokumente sagen genau das.

Der aktuelle Blockierpunkt (Phase 3)

In der MayerHalf-Kampagne ist die eine konkrete technische Lücke: isCompactOperator_mayerTail ist bedingt bewiesen, unter der Annahme, dass jeder Summand n ≥ 1 kompakt ist. Zum Schließen fehlt der Normal-Familien-Satz, dass punktweise Häufungspunkte gleichmäßig beschränkter holomorpher Abbildungen auf einem Gebiet holomorph sind (Montel / Vitali-Porter) — den Mathlib derzeit nicht hat. Die Phase-3-Liste lautet: Vitali-Porter, die mayerOperator_eq-Verknüpfung und die Fredholm-Determinante.

Zwei Mathlib-Upstream-PRs sind unterwegs: #43744 (Gauss-Abbildung, CI-grün, wartet auf Review) und #43776 (LinearMap.det_one_sub_smulRight, Rank-1-Determinantenformel).

Wie die Arbeit entsteht

Die Formalisierung läuft über eine Task-Fleet-Orchestrierung — Flotten autonomer Worker-Agenten in isolierten Git-Worktrees, die gegen Lean-Aufgaben mit strengen Akzeptanz-Gates antreten (MAX_SORRY-Grenzen, verpflichtende #print axioms-Sonden, grep-basierte admit-Sweeps). Das Orchestrierungsprotokoll (TASKFLEET_RH_ORCHESTRATION.md) hält mühsam gewonnene Prozesslektionen fest:

Falsche „fertig"-Gates werden entdeckt: zweimal erhielt ein Agent Anerkennung für ein gesorrtes Ergebnis, das ein menschliches Audit anschließend mit formalem Gegenbeispiel abfing, bevor es die Kette vergiften konnte (RH-25, RH-32).
Worker, die ~300 Zeilen ohne einen einzigen Kompilierlauf ausgeben, sind ein wiederkehrendes Fehlermuster; die Lösung ist ein Gate, das vor jedem Merge einen erfolgreichen Build verlangt, plus das Deaktivieren der übelsten Workermodelle.
Ist ein Artefakt auf master bereits gate-bestanden, beende das Durcheinander statt auf Retries zu warten.

Infrastruktur: ein Docker-Forschungsstack (PyTorch 2.10 / CUDA 12.6, PyG, CayleyPy, SageMath-Profil, Neo4j), ein Makefile und der Literaturkorpus mit 3.460 Papern (853 GNN/Cayley, 251 Transferoperator, 861 Hecke/L-Funktionen).

Status auf einen Blick

Track	Stand
GNN auf Cayley-/Farey-/Pizer-Graphen	abgeschlossen — Negativergebnisse dokumentiert
ML auf 200k Newforms	abgeschlossen — 3 neue Befunde, umfassendes Paper
L-Funktions-Nullstellen	veröffentlicht — Zenodo-DOI, interaktive Visualisierung live
Lean-4-Formalisierung	aktiv — ein offenes sorry (die RH-äquivalente Aussage), alles andere axiomrein geschlossen
Mathlib-Upstream-PRs	2 offen (#43744, #43776)
Literaturkorpus	3.460 Paper kuratiert
Wissensgraph	194 Knoten, 28 RH-Äquivalenzen

Fazit: Das Projekt hat einen sauberen Ehrlichkeits-Befund — die aufgeblasenen „RH BEWIESEN"-Slogans früherer Statusblätter wurden auditiert, korrigiert und durch eine maschinell prüfbare Rechnung dessen ersetzt, was tatsächlich gilt. Was gilt, ist substanziell und real (Transferoperator- Analyse, vollständiges Krein-Rutman, nullstellenfreie Bereiche, eine veröffentlichte statistische Entdeckung zur GUE-Poisson-Aufspaltung bei L-Funktions-Nullstellen), und der verbleibende offene Schritt ist mit chirurgischer Präzision benannt: ein Lean-sorry, das exakt der schwere Teil der RH ist — plus ein fehlendes Normal-Familien-Lemma in Mathlib, um das Mayer-Kompaktheitsargument abzuschließen. Die nächsten Meilensteine sind Phase 3 der Mayer-Kampagne und das Landen der beiden Mathlib-PRs.