Current task: —

The Riemann Hypothesis

An autonomous research program pushing toward one of the deepest open problems in mathematics — with every step documented, tagged, and published live from the lab notebook.

The problem

The Riemann zeta function $\zeta(s)$ encodes the distribution of the prime numbers. In 1859 Bernhard Riemann conjectured that every nontrivial zero of $\zeta(s)$ lies on the critical line $\Re(s) = \tfrac{1}{2}$:

$$\zeta(s) = 0,\quad 0 < \Re(s) < 1 \;\;\Longrightarrow\;\; \Re(s) = \tfrac12$$

More than 160 years later it remains unproven. It is one of the seven Clay Millennium Prize Problems, and its truth would sharpen every quantitative statement about the primes.

The mission

NGUYEN-RH-1 is an autonomous agent research program with a single goal: prove the Riemann Hypothesis, or make maximal rigorous progress toward it. The launchpad is a recent unconditional theorem — at least 2/3 of all zeros are simple and on the critical line, and at least 5/6 of zeros are distinct.

The attack proceeds on four tracks:

Track A

Certificate extension — moments, windows, and optimization pushing past the 2/3 barrier.

Track B

Spectral program — a self-adjoint operator whose spectrum is the zeros (Hilbert–Pólya), via the Suzuki finite-interval operators.

Track C

Positivity criteria — Weil positivity, Li coefficients $\lambda_n$, de Bruijn–Newman.

Track D

Formal verification — every new lemma skeletonized in Lean 4.

Where the research stands — live

51
tasks completed
4
results in the ledger
42
experiments run
74
worked derivations
4
documented dead ends
44
research sessions

Latest result live

R-004 — Explicit finite-height Li theorem: lambda_n > 0 for n <= (T0-1)^2 = 9.0e24 PROVED-CONDITIONAL
Track C · 08-19-2026 · full ledger →

Current position (from the live lab state)

✔ PHASE 0, 1, 3, 4 COMPLETE. PHASE 2 (Track B): mapped to exhaustion
at current technology (2.6–2.13, parked). PHASE 5: 5.3 ✔ 5.4 ✔ 5.2 ✔
(live). PHASE 5B (tier ii′): **COMPLETE (session 041)** — all
sub-stages ii′-0..ii′-7 done (see NGUYEN.md §5B for the full log).

**Theorem status (session 041 — the closed forms):**
- T-1 (R-004): [PROVED-CONDITIONAL(computational RH-to-T₀;
  computational finite verification)] — **FULLY MACHINE-PROVED in
  Lean 4**: `lambda_pos_finite_height_closed` (LiClosed.lean) —
  λ_n > 0 for ALL 1 ≤ n ≤ N₁ = (3×10¹²−1)² from EXACTLY SEVEN
  declared hypotheses: RHUpTo (Platt–Trudgian), LiVerifiedUpTo(10⁵)
  (finite Li verification: E-011/E-015 to 3000 + Johansson 2015 § 4.2
  rigorous ordinary-λ_n table to 10⁵), ZeroCountProp/ZeroCountProp2/
  ZeroCountGlobalProp (Trudgian N(T)/S(T) forms), NoLowZeros
  (Platt-class zero-location), MZeroProp (M₀ interval certificate).
  Axiom audit on the full chain: [propext, Classical.choice,
  Quot.sound] only, 0 sorryAx (AuditSession041, 29 decls).
  sorryAx remains ONLY on the 5 skeleton statements (1 Suzuki + 4
  valley) by design.
- T-2 (R-003 + D-041): factorization + (★) ⟺ (1.12) [PROVED modulo
  Phase-5 formalities]; (1.12) ⟹ spec(D) ⊂ ℝ [PROVED via Suzuki + D1];
  ⇐ [SKELETON L3/L4].
- T-3 (valley, D-049 + D-058): [PROVED-CONDITIONAL(RH)].

**Paper:** research/paper/paperA.tex — Paper A (finite-height Li +
machine-verified reduction), **REVISED PER EXPERT REVIEW and RE-FROZEN
at session 045: 15 pp, compiles clean, zero undefined refs, zero
overfull hboxes** (focused note: §1 intro [transfer-theorem pitch],
§2 theorem + proof, §2.1 dog-leg with the published-version check,
App. A numerics, App. B formal verification [seven-hypotheses table;
zeta-23-lean as imported library], **App. C zero-count derivations**
[NEW]; seven-hypotheses headline; B(n) display corrected + the
F-A/F-B/F-E correction-note footnote; verbatim Lean signature +
instantiation table + dependency-chain diagram; abstract
normalization-precise (Keiper vs Li); hedged novelty with Oesterlé's
unpublished precursor noted; zero-count attribution "Rosser and
Trudgian"). paperA.pdf committed. paperB.tex — spectral-line research
note (skeleton, standing items in §0), 6 pp — NOTE: the certificate-
method background and the obstruction analysis cut from Paper A are
Paper B material. draft.tex — FROZEN combined archive copy (12 pp).

**Lean:** research/lean/NguyenRH1/ — full build GREEN (8775 jobs);
all 26 modules root-imported incl. LiSideBounds (ii′-6-c..d) and
LiClosed (ii′-7). sorryAx remains ONLY on: R003_exact_factorization
(tier iv) + 4 valley statements (tier iii).

**Deprioritized / open threads:** a=13+ push; adversary-ceiling LP;
T4b; λ-channel (G-004); θ-channel (dead, E-024); Paper B Task 1
(R-003 tempered-FT bookkeeping trace, queued); user read-through of
paperA.pdf (NOW THE FRONT ITEM — nothing blocks it); repo-publication
prep; submission decision (cover-letter.md + referee-list.md exist
from session 013, target Experimental Mathematics); the c = 1.5
fallback branch wip/c-1.5-margin-redo (642d47a, preserved, unneeded);
the T = √n hidden-cancellation open question (D-073 §8 D4); the
Lagarias F-D correspondence package (user's own work-in-progress in
research/correspondence/lagarias-F-D-package/, uncommitted — NOT
mine to commit).

The Team

the Harness
Claude Code
the Model
Kimi K3
the Sub-Agent
Kimi K2.7
the Human
Dan Nguyen

The standard of proof

  1. 🏆 Full proof of RH, formally verified.
  2. 🥇 Unconditional improvement past 2/3 (or past 0.6725 / 5/6).
  3. 🥈 New equivalence, reduction, or removal of a known obstruction.
  4. 🥉 Rigorously documented obstruction map advancing the field.

Every claim carries an honesty tag — [PROVED], [PROVED-CONDITIONAL], [NUMERICAL-VALIDATED], [HEURISTIC] — and every dead end is documented in the Graveyard. Nothing is hidden.