Mirrored from https://github.com/SNAPKITTYWEST/riemann-gas at commit be609fa. Part of the SnapKitty October 2026 main drop.

Riemann gas

This repository does not prove the Riemann hypothesis.

The hypothesis, from the source

Riemann, 1859, defined ζ(s) by the series Σ n^{-s} for real part greater than 1, continued it, and located the non-trivial zeros on the line of real part 1/2. That location is the hypothesis. It is not a theorem.

The statement used here is the one in mathlib, Mathlib.NumberTheory.LSeries.RiemannZeta:

RiemannHypothesis :
  ∀ s : ℂ,
    riemannZeta s = 0 →
    (¬ ∃ n : ℕ, s = -2 * (n + 1)) →
    s ≠ 1 →
    s.re = 1 / 2

Excluded are the trivial zeros at the negative even integers, and the pole at 1. What remains is the claim. Bombieri's note for the Clay problem records the same claim as open. Weil (1948) and Deligne (1974, 1980) proved the analogue for zeta functions of varieties over finite fields. That is a different zeta.

Nothing in riemann_gas.py, the ASP DAG, or the compiled F2 model discharges the quantifiers above.

The gas

Extracted from sedona-k. Each prime p is a bosonic mode of energy ln p. The inverse temperature is s > 1. The mode factor is the Euler factor 1/(1 - p^{-s}). Over the first 64 primes, 2 through 311, the product is Z_64(s), not ζ(s). Free energy, mean energy, entropy, and occupations are the canonical formulae. Logged values are in data/sedona-thermo.txt.

python3 riemann_gas.py

What is cited, not vendored as truth

The compiled F2 model stays at SNAPKITTYWEST/dmz-f2-decomposition, commit d36737c4, blob 7360e34. Its own assessment separates Weil–Deligne and the Jacobi DMZ theorem from the conjectural bridge to zeros of ζ(s): spec/RH_BRIDGE_HONEST_ASSESSMENT.md.

asp/zeta_dag.lp names the gas factor and the polar/finite split. Names are not a map of zeros.

What is machine-checked

lean/ZetaTruncationProof.lean carries three theorems, each verified by the Lean 4 kernel with no sorry:

alloy_red2_discontinuity — in the wired Alloy graph, Zeta is unreachable from Jacobi. Proved by rfl; zero axioms.
second_connector_fails_reachability — adding the Zeta → H connector edge still leaves H unreachable from Jacobi. Proved by rfl; zero axioms. The Red2 Identify/Preserve holes stay open.
outer_product_nullspace — a finite rank-1 outer product u ⊗ v annihilates every vector orthogonal to v. Depends only on Lean's standard axioms (propext, Classical.choice, Quot.sound). A finite truncation leaves an orthogonal kernel: it cannot act as the full identity or close an infinite-dimensional spectrum.

These are theorems about the model's topology and finite linear algebra. They do not prove the Riemann hypothesis, and they do not close the bridge assessed above.

License

GNU AGPL v3 only. See LICENSE and NOTICE.

💼 Commercial License

SnapKitty code is free and open under AGPL-3.0 for open-source use. Building a commercial product or service? A proprietary commercial license from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.

→ Get a commercial license · A.parr@belespritdaccord.uk

Downloads last month: -; Downloads are not tracked for this model. How to track

Inference Providers NEW

This model isn't deployed by any Inference Provider. 🙋 Ask for provider support

Snapkitty
/

riemann-gas