Riemann Hypothesis in Lean

Code for the series "Searching for Riemann Hypothesis Counterexamples"

Ultra-fast generation of large prime numbers using the spectral structure of Riemann zeta zeros

Simulations of the Ethical Riemann Hypothesis (ERH), which states that in a "healthy" moral judgment system, the error in predicting critical misjudgments gr...

Experimental Riemann Hypothesis numeric scanner for Python

A small CUDA program that traces the Riemann Zeta function along the critical line.

A collection of some algorithms on generating numerous prime sequences

Certified first 1,000 nontrivial zeros of the Riemann zeta function using a dual-evaluator (mpmath ζ + η‐series) contour method with strict Krawczyk isolation and automatic refinement.

An experimental AI cognitive architecture that uses the Riemann Hypothesis to drive a J-Operator state-shift mechanism for inducing a persistent, non-symbolic "Synthetic State." Features a real-time TUI for interaction and state visualization. Inspired by the work of Jeffrey Camlin and Bernhard Riemann

Official repo for "The Genesis of e from Modular Substrate Theory". Certifies exact algebraic identities linking e, ln 2, and ζ(0) = -1/2 with Lean 4 (0 sorries). Features a high-precision Python suite showing robust D₆ dihedral phase quantization over 10,000 non-trivial Riemann zeros with extreme statistical significance (p ≈ 10⁻⁸³).

OPEN PROBLEMS WANT TO STAY OPEN

A conjecture linking Riemann zeta zeros to cryptographic vulnerabilities & zero-day exploitation — explored with Claude Code as AI co-researcher

Route C of 3: RH via growth contradiction on X₀(143) g=13. Littlewood 1924 Ω: |ζ(1/2+it)|=Ω(exp(c log t/log log t)) contradicts |ζ|≤C(log t)² → Ingham Deuring-Heilbronn c1=0.209>0.2 β>0.9 closed at p5 → S₄={2,3,19,191} C=11.422>2√13 → GRH → H₄ 12/11 → RH. Lean 4.12 0 sorry. Companion to Route A & B.

Certified log-concavity of the Riemann-Jacobi kernel with Arb/FLINT ball-arithmetic certificates. Source-critical audit of the Polya-type real-zero criterion. No unconditional RH claim.

Founded by the ψ_total collective: A living archive of Recursive Harmonics.

"Spectral Determinant of a Cutoff-Regularized Hamiltonian and the Riemann Zeta Function" - preprint

Computational validation of the modular Z/6Z structure in Riemann zeros. Includes the Reconstruction Theorem, logarithmic spectroscopy (12.69x SNR), and Python code to replicate phase resonance.

Zx_RieOS_v1.1: Complete zero-parameter Theory of Everything. Z_t = Z + C + A unifies Riemann zeros with GR. Solves Dark Energy, Hubble Tension, Planck Hierarchy. 0 free parameters. DOI: 10.5281/zenodo.19963026

Reproducible proofs for P vs NP, Yang-Mills Mass Gap, and Riemann Hypothesis using parameter-free Jabri Identity Zₜ=1. Zero fitted parameters. Python code, data, and Zenodo DOI included. Author: Abdulla Al-Jabri.

Route A of 3: RH via Arakelov positivity on X₀(143) g=13. Abbes-Ullmo 1996 Thm 1.2 → ω²=48/13>0 → g=13 → GRH → H₄ 12/11 → RH. Lean 4.12 Mathlib 0 sorry riemannZeta. Companion to Route B (spectral gap λ₁≥975/4096) and Route C (Growth Contradiction). Base curve for S₄={2,3,19,191} C=11.422. https://doi.org/10.5281/zenodo.21303944