The Riemann Project, September 2026 — An Honest Status Report | Research

The Riemann Project, September 2026 — An Honest Status Report | Research | Tobias Weiss

What this project is

A multi-track research effort attacking the Riemann Hypothesis (RH) from the computational and machine-verified side. The unifying idea is the chain

Cayley-graph eigenvalues → Hecke eigenvalues → L-functions → ζ(s)

and the project attacks it along four parallel tracks:

GNN experiments on arithmetic graphs (Cayley graphs of SL(2,𝔽_p), Farey graphs, Pizer graphs) — with largely negative, but scientifically valuable, conclusions.
Data-driven ML on LMFDB data — the most successful track, producing a published paper and three new empirical findings.
L-function zero statistics — a 63,844-form spectral-statistics study that is already archived on Zenodo with a DOI.
A Lean 4 formalization of a transfer-operator approach to RH — the current frontier of the project's active work.

A Neo4j knowledge graph (194 nodes, 161 relationships, 28 RH equivalences) encodes the theory chain, a 3,460-paper literature corpus is curated in literature/, and an interactive three.js visualization is deployed on GitHub Pages.

Track 1 — GNNs on arithmetic graphs: mostly negative, and that is the point

Seven experiment tracks asked whether GNNs can predict spectral or number-theoretic invariants from graph structure alone. The answer is consistent: GNNs learn within their training distribution but fail to generalize across primes.

Track	Graph	Target	Baseline R²	GNN R²	Verdict
1	Cayley SL(2,𝔽_p), subgraphs	spectral gap	—	< 0	failed
2	Cayley SL(2,𝔽_p), full graph	spectral gap	0.782	0.824	marginal
3	Farey graph	spectral gap	0.9999	−7.57	trivial
4	Cayley, 1 generator	Hecke eigenvalues	0.41	−0.21	failed
5	Cayley, 10 generators	Hecke eigenvalues	0.977	−0.32	failed
6	Cayley, 10 generators	spectral gap	0.43	−2.12	failed
7	Pizer graphs (Hecke T₂)	T₃ eigenvalues	0.057	0.000	zero generalization

The failures are mathematically explained, not fixable by tuning:

Cayley graphs are vertex-transitive. Every node sees an identical local structure (degree 4, same clustering), so local neighborhoods carry zero information about global spectral properties. Any subgraph-based approach is doomed in principle.
The Farey spectral gap follows a perfect power law gap ≈ 2.65/n^(0.999); a log-log linear baseline hits R² = 0.9999 (0.07% median error). No model can meaningfully beat a closed-form law.
The one partial success — full-graph ChebConv with Random Positional encoding, R² = 0.824 vs. 0.782 baseline — is a real effect (relative prediction error mostly below 8% for p ≥ 37, best 0.3% at p = 37 — with noisy outliers like p = 31 at 18.7%), but the ΔR² of +0.042 over the log(N) trend carries no number-theoretic signal.

Lesson recorded in the project: distinguishing params of a graph family are global (size, generator set), and learned "explanations" from local structure are not arithmetic. These may be the first systematic negative results at the GNN × number theory interface.

Track 2 — ML on 200,000 newforms: the productive pivot

After the Cayley failures, the project pivoted to data scaling: 200,000 weight-2 newforms from LMFDB, 100 Hecke trace coefficients each. This track produced the project's strongest results (see also the comprehensive modular forms paper):

Analytic rank classification: F1 = 0.970
Dimension regression: R² = 0.990
CM form detection: F1 = 0.919 (the M₄/M₂ moment ratio is the single most discriminative feature)
First L-function zero prediction from a trace-index graph construction (newforms connected via shared eigenstructure): a ChebConv GNN reaches R² = 0.631, and an architecture search finds GATConv at R² = 0.731 (+15.9% over the ChebConv result).

Three new empirical findings came out of this, after fixing a normalization error in the Sato–Tate moment analysis:

Galois Correlation Constant ρ₂ = −0.607 ± 0.012 — an anti-correlation between conjugate Hecke eigenvalues in dimension-2 non-CM forms, with a dilution law ρ_d ~ d^(−1.29).
Dimensional Scaling Law M₂(d)·d → 0.177 + O(1/d) — a direct empirical probe of Sato–Tate group structure across Hecke-field degrees.
CM classifier F1 = 0.919 (as above).

Track 3 — L-function zero statistics: the dimension split

The statistical study now archived on Zenodo (DOI 10.5281/zenodo.21974748) analyzes 63,844 weight-2 newforms (568,708 nearest-neighbor zero spacings), fitting the Brody distribution β per form and splitting by Hecke-field dimension:

Group	β (MLE)	Interpretation
All forms, aggregate	0.620	"intermediate" — misleading
dim = 1 (CM)	1.879	GUE-like (KS distance 0.017)
dim ≥ 2 (non-CM)	0.242	near-Poisson
rank 0 / rank 1	0.676 / 0.538	intermediate

The headline: the aggregate "intermediate" repulsion is a mixing artifact. CM forms (~15% of the population) are essentially GUE; non-CM forms (~85%) show dramatically weakened — near-Poisson — level repulsion. A deep-dive confirmed the 1,748 "GUE outliers" among dim ≥ 2 are genuinely repulsive (pooled Brody β) and that CM status explains only 1.1% of them (3.58× enrichment, but 102 forms) — level and root number matter more. This contradicts the folklore that all L-function zeros converge to the same random-matrix limit. Full details in The Dimension Split in L-Function Zero Statistics.

Interactive versions of these findings (ζ landscape, critical line, Brody waterfall through the phase transition) are live at tobias-weiss-ai-xr.github.io/riemann/.

Track 4 — Lean 4 formalization: where the project actually lives now

The current active frontier is a machine-verified formalization of the transfer-operator route to RH in Lean 4 / Mathlib, 38 modules under lean/Riemann/. The honest accounting is maintained in research/FRONTIER.md and lean/Riemann/AxiomAudit.lean — every load-bearing declaration carries a #print axioms dependency bill.

What is genuinely, axiom-cleanly proven

All of the following depend only on the standard [propext, Classical.choice, Quot.sound]:

The Gauss-map / Ruelle transfer operator L_s on C([0,1], ℂ) is a bounded operator with explicit constant ‖L_s‖ ≤ Σ (n+1)^(−2·Re s) = ζ(2·Re s), together with full summability groundwork.
Uniform convergence of the partial sums — plus the honest correction that compactness is false on C([0,1]) (the n = 0 branch violates equicontinuity; compactness belongs on an analytic class like the disc algebra).
Euler-region and Re s ≥ 1 nonvanishing of ζ (trivial-classical, inherited from Mathlib), trivial-zero exclusion via the functional equation, and the functional-equation reflection ζ(ρ) = 0, 0 < Re ρ < 1 ⇒ ζ(1−ρ) = 0.
Krein–Rutman in full (RH-39): after catching and removing two admitted false lemmas with formal counterexamples (a collapse lemma; a real Gelfand upper bound refuted by Complex.I), the weak and strong forms are proved unconditionally — the last gap was closed by a direct resolvent blow-up argument that made the whole β-stabilization machinery obsolete.
Real Gelfand formula for positive operators (RH-38, sorry-free) — the upper bound that unblocks the resolvent-positivity endgame.
Mayer half-disc algebra phase 2 (RH-40/41/42): the disc algebra and the half-disc algebra as complete subalgebras of continuous functions (Weierstrass closure proved), the Mayer transfer summands with ‖T_n‖ ≤ 1/(n+1)², and the compact tail assembly — all gate-clean, 0 sorries.

The exact frontier: one sorry, equivalent to RH

The repository carries exactly one open sorry at lean/Riemann/TransferOperator/Complete.lean:152:

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

This statement — no zero in the strip 1/2 < Re ρ < 1 — is equivalent to the hard half of RH (the FE reflection turns it into the full critical-strip statement). Everything else downstream that looks like a "proof" of RH is honestly labeled:

fredholmDet is a definitional model — ζ(2s)/C(s) by definition, not det(1−L_s). "Mayer's identity" holds by unfolding, not by spectral theory.
modelLeadingEigenvalue = exp(1/2 − s) is a model, chosen so the wanted unit-disk inequalities hold by calculus; it is not the spectrum of L_s.

The honest upgrade path to close the frontier is: (1) Mayer's analytic class — done in phase 1–2; (2) a genuine trace-class Fredholm determinant and Mayer identity on it; (3) Krein–Rutman/ρ(L_s) < 1 down to Re s > 1/4 — each step is exactly as hard as the corresponding half of RH. No free lunch, and the project's own documents say so.

The current blocking point (phase 3)

In the MayerHalf campaign the one discrete technical gap is: isCompactOperator_mayerTail is proven conditionally on every summand n ≥ 1 being compact. Closing it needs the normal-families fact that pointwise cluster limits of uniformly bounded holomorphic maps on a domain are holomorphic (Montel / Vitali–Porter) — which current Mathlib lacks. The phase-3 queue is: Vitali–Porter, the mayerOperator_eq assembly, and the Fredholm determinant.

Two Mathlib upstream PRs are in flight: #43744 (Gauss map, CI-green, awaiting review) and #43776 (LinearMap.det_one_sub_smulRight, rank-1 determinant formula).

How the work gets done

The formalization is executed by a task-fleet orchestration — fleets of worker AI agents in isolated git worktrees, dispatched against Lean tasks with strict acceptance gates (MAX_SORRY limits, mandatory #print axioms probes, grep-based admit sweeps). The orchestration log (TASKFLEET_RH_ORCHESTRATION.md) records hard-won process lessons:

False-done gates get caught: twice, an agent received credit for a sorried result that a human audit then caught and counter-exampled before it poisoned the chain (RH-25, RH-32).
Workers that emit ~300 lines without compiling once are a recurring failure signature; the fix is a gate that requires a successful build before any merge, and disabling the worst-offending worker models.
When an artifact is already gate-passed on master, stop the churn instead of waiting out retries.

Infrastructure: a Docker research stack (PyTorch 2.10 / CUDA 12.6, PyG, CayleyPy, SageMath profile, Neo4j), a Makefile, and the 3,460-paper literature corpus (853 GNN/Cayley, 251 transfer-operator, 861 Hecke/L-function papers).

Status at a glance

Track	State
GNN on Cayley/Farey/Pizer graphs	completed — negative results, documented
ML on 200k newforms	completed — 3 new findings, comprehensive paper
L-function zero statistics	published — Zenodo DOI, interactive viz live
Lean 4 formalization	active — one open sorry (the RH-equivalent statement), everything else axiom-clean
Mathlib upstream PRs	2 open (#43744, #43776)
Literature corpus	3,460 papers curated
Knowledge graph	194 nodes, 28 RH equivalences

Bottom line: the project has a clean bill of health on honesty — the hyped "RH PROVEN" slogans of earlier status sheets were audited, corrected, and replaced by a machine-checkable account of what actually holds. What holds is substantial and real (transfer-operator analysis, full Krein–Rutman, zero-free regions, a published statistical discovery about GUE vs. Poisson splitting in L-function zeros), and the remaining open step is stated with surgical precision: one Lean sorry that is exactly RH's hard half — plus one missing normal-families lemma in Mathlib to finish the Mayer compactness argument. The next milestones are phase 3 of the Mayer campaign and landing the two Mathlib PRs.