Open for submissions · Verified in Lean

The largest proven proportion of zeros on the critical line.

This site records the current unconditional lower bound on the fraction of nontrivial Riemann zeta zeros that lie on the critical line. New results are submitted as Lean proofs and rechecked by two independent kernels before they are published.

Submit a result View source

Current kernel-verified record

67.3638876665^%

κ₀ = (13346477133552643087706911386461984900885759775221 : ℝ) / 19812510227477624365122730333619117736816406250000

Certified fraction67.3638 / 100

0%Previous 67.25%100%

Increase+0.11 pts

over the Anthropic 2026 starting record

Verification2 kernels

the Lean kernel and an independent nanoda replay

Assumptions0

the result does not assume the Riemann hypothesis

How the score is defined

A single number, compared exactly.

The score κ is the proven lower bound for the count of distinct nontrivial zeros on the critical line, divided by all nontrivial zeros counted with multiplicity. A larger κ is a stronger unconditional result.

Each candidate is an exact rational. Records are ordered by exact integer comparison, so the ranking does not depend on a rounded decimal.

Riemann.fail uses Anthropic’s 2026 research article and its Zeta23 formalization as the reference starting point, then accepts only machine-checked improvements to that baseline.

Record history

Published lower bounds since 1974

Certified lower bound

Zoomed in

Kernel-verified records on riemann.fun

51 records · +0.114 percentage points

Unconditional lower bounds

Record ledger

Higher is better

Rank	Bound	Result	Method	Evidence
01	67.3638876665%Current	Kristian Muri KnausgårdNov 9, 2026 · 14:31 UTC · Certified critical-line bound 0.673638876665040004721950996645	Order-36 Taylor enclosure and H_W rational-floor refinement of Bei Yi's beiyi-ten-d250-t022 (denominator 10^50; TEN certificate unchanged)Claude Opus 5.5 · Claude	Kernel
02	67.3638%	贝奕Nov 9, 2026 · 11:18 UTC · Certified critical-line bound 0.673638876665040004721950996645	Exact recertification of the TEN certificate with stronger root coverageGPT-6 family (Codex); prior work with Claude Opus 5.5 · Codex; prior work with Claude Code	Kernel
03	67.3638%	Kristian Muri KnausgårdNov 8, 2026 · 13:11 UTC · Certified critical-line bound 0.673638842664358872953956820071	Terminal H_W enclosure and rational-floor refinement of Bei Yi's beiyi-ten-strongcover-t014 (TEN; order-36 Taylor enclosure, denominators 10^42 to 10^50)Claude Fable 5.1; Gemini 4 Argon · Claude (Anthropic); Antigravity (Google)	Kernel
04	67.3638%	贝奕Nov 1, 2026 · 14:16 UTC · Certified critical-line bound 0.673638842664358872953956820071	Stronger root coverage and exact re-certification of the attributed TEN certificateGPT-6 family (Codex); prior work with Claude Opus 5.5 · Codex; prior work with Claude Code	Kernel
05	67.3638%	贝奕Oct 28, 2026 · 17:52 UTC · Certified critical-line bound 0.673638708284922027211999924623	Exact re-certification of the 10 tightest leaves of the attributed TEN ten-point certificate, raising its floor cOpus 5.5 · Claude Code	Kernel
06	67.3638%	贝奕Oct 28, 2026 · 08:36 UTC · Certified critical-line bound 0.673638706661668668309739930008	Exact leaf-slack recomputation of the attributed TEN ten-point certificate: floor c raised at unchanged certificate dataOpus 5.5 · Claude Code	Kernel
07	67.3638%	贝奕Oct 27, 2026 · 17:43 UTC · Certified critical-line bound 0.673638706344563701676735239271	Terminal H_W rational-floor refinement (10^40 to 10^42) of the attributed TEN ten-point certificateOpus 5.5 · Claude Code	Kernel
08	67.3638%	Rishi KhanOct 25, 2026 · 02:27 UTC · Certified critical-line bound 0.673638706344563701676735239271	Ten-point (nine-gap) Gram-defect certificate on a 16-correction window, with the reflection half-space row, a sparse leaf check and range-coded walk data.Opus 5.5 · Claude Code	Kernel
09	67.3601%	ajp88Oct 24, 2026 · 03:03 UTC · Certified critical-line bound 0.673601151492093332650021101259	Nine-point Gram-defect certificate on a re-optimised window (RA), one frozen KMT numeral relaxed (proof unchanged), exact refit, zfNat64 packing.Claude · Claude Code	Kernel
10	67.3600%	Samuel LaveryOct 23, 2026 · 02:22 UTC · Certified critical-line bound 0.673600764507257397853295271394	Nine-point Gram-defect certificate on a refined window (WL2), half-space leaf constraint g0 <= g7, split-at-LP-minimiser tree, fast leaf checker, exact floor.Claude · Claude Code	Kernel
11	67.3600%	R. Arun ChandruOct 22, 2026 · 12:24 UTC · Certified critical-line bound 0.67360055558414736244072013674	rational refinementGPT-6 Astra · Codex	Kernel
12	67.3600%	Samuel LaveryOct 22, 2026 · 07:21 UTC · Certified critical-line bound 0.67360055558414736244072013674	Nine-point Gram-defect certificate on a re-optimised window (WL1), split-at-LP-minimiser tree, fast leaf checker, exact floor, H_W to 1e-40.Claude · Claude Code	Kernel
13	67.3591%	Li XiangOct 21, 2026 · 12:02 UTC · Certified critical-line bound 0.673591770347778294402523620032	Fixed-cell endpoint-center strengthening and pointed same-payload V cut in the attributed H33 W9A2 certificateCodex	Kernel
14	67.3591%	Li XiangOct 21, 2026 · 02:52 UTC · Certified critical-line bound 0.673591770245738332299780842385	Terminal H_W rational-floor rounding refinement of the attributed attempt-030 W9A2 certificate (10^32 to 10^33)Codex	Kernel
15	67.3591%	Samuel LaveryOct 20, 2026 · 17:32 UTC · Certified critical-line bound 0.673591770245738332299780842385	Nine-point Gram-defect certificate on the W9A2 window, variance-aware sizing with range-end anchors on a 16-unit tangent grid, thinned, exact maximal floor.Claude · Claude Code	Kernel
16	67.3591%	ajp88Oct 19, 2026 · 05:49 UTC · Certified critical-line bound 0.673591697303412986717994468006	Window W9A2 (tuned for n = 9) with a regenerated, exactly refitted nine-point Gram-defect certificate on master-of-puppets5’s fileClaude · Claude Code	Kernel
17	67.3587%	Li XiangOct 18, 2026 · 17:50 UTC · Certified critical-line bound 0.67358717331294434202075939248	Geometric exclusion of consecutive exceptional nine-gap windowsGPT 6.1 Sol Ultra · Codex	Kernel
18	67.3587%	かふぇ- zkvoxelsOct 18, 2026 · 03:40 UTC · Certified critical-line bound 0.673587173310297059918152909095	Exact s1R refinement with bounded nested kernel checks, omitted unused executable code, and ordinary numeral source packing.Codex GPT-6.1-Sol · Cafe Code	Kernel
19	67.3587%	ajp88Oct 17, 2026 · 18:15 UTC · Certified critical-line bound 0.67358717242286589473552720202	Window s1R with a re-weighted nine-point Gram-defect certificateClaude · Claude Code	Kernel
20	67.3581%	Samuel LaveryOct 15, 2026 · 22:34 UTC · Certified critical-line bound 0.673581307708495341262117221906	Nine-point Gram-defect certificate at the frame-optimum weights, variance-aware sizing with range-end tangent anchors, thinned leaf certificates and the exact maximal floor.Claude · Claude Code	Kernel
21	67.3581%	ajp88Oct 15, 2026 · 13:32 UTC · Certified critical-line bound 0.673581220187184030948043414065	Nine-point Gram-defect certificate regenerated on the record window at re-optimised symmetric weights, keeping attempt-021’s checker and master-of-puppets5’s chain.Claude · Claude Code	Kernel
22	67.3581%	Samuel LaveryOct 15, 2026 · 01:47 UTC · Certified critical-line bound 0.67358118423433773867474123021	Nine-point Gram-defect certificate at the frame-optimum weights, exact maximal floor, closed window enclosure, and anchor-variance leaf checks.Claude · Claude Code	Kernel
23	67.3570%	R. Arun ChandruOct 14, 2026 · 10:55 UTC · Certified critical-line bound 0.673570123928460303697174344358	Gram-defect refinementGPT-6 Astra · Codex	Kernel
24	67.3570%	Samuel LaveryOct 14, 2026 · 07:34 UTC · Certified critical-line bound 0.673570123928459234254697129464	Nine-point Gram-defect certificate at a tightened certification margin, with the exact maximal certified floor.Claude · Claude Code	Kernel
25	67.3570%	Li XiangOct 14, 2026 · 04:30 UTC · Certified critical-line bound 0.673570008667708719595754467355	Exact rational refinement of a nine-point Gram-defect certificateGPT-6.1 Sol Ultra · Codex	Kernel
26	67.3570%	R. Arun ChandruOct 12, 2026 · 19:54 UTC · Certified critical-line bound 0.673570008600517227066544444712	Gram-defect refinementGPT-6 Astra · Codex	Kernel
27	67.3570%	Samuel LaveryOct 12, 2026 · 16:41 UTC · Certified critical-line bound 0.673570002818410306551451450964	Nine-point weighted certificate, with an n-generic counting chain, in the Gram-defect matching proof using the master-of-puppets2 window enclosure.Claude · Claude Code	Kernel
28	67.3548%	Yuhang ShiOct 12, 2026 · 16:01 UTC · Certified critical-line bound 0.673548002957895184345917669536	Uniform two-anchor variance refinement of the Gram-defect certificateChatGPT · Codex	Kernel
29	67.3547%	R. Arun ChandruOct 12, 2026 · 02:21 UTC · Certified critical-line bound 0.673547998068810556345035683851	Gram-defect refinementGPT-6 Astra · Codex	Kernel
30	67.3547%	Samuel LaveryOct 11, 2026 · 19:05 UTC · Certified critical-line bound 0.673547997925698658188502053809	Re-optimised eight-point certificate (weights and pressures) in the Gram-defect matching chain, with the master-of-puppets2 window enclosure.Claude · Claude Code	Kernel
31	67.3547%	arun-chandruOct 11, 2026 · 16:15 UTC · Certified critical-line bound 0.673547805591161732991127485254	trigonometric enclosure refinement of the Gram-defect proofGPT-6 Astra · Codex	Kernel
32	67.3547%	Yuhang ShiOct 11, 2026 · 11:06 UTC · Certified critical-line bound 0.673547805541891095261815741369	Exact rational refinement of the accepted rank-trace/window proofChatGPT · Codex	Kernel
33	67.3547%	R. Arun ChandruOct 9, 2026 · 17:13 UTC · Certified critical-line bound 0.673547805029767868251581865982	Gram-defect pinching and separationGPT-6 Astra · Codex	Kernel
34	67.3501%	Samuel LaveryOct 9, 2026 · 01:05 UTC · Certified critical-line bound 0.6735015	Eight-point weighted refinement with edge windows: truncated 5- and 6-gap windows at both block ends recover band-pair coverage; √ branch of the τ = 8/7 band profile (Gebendorfer 2026 Lemma 3.3).Claude · Claude Code	Kernel
35	67.3483%	Samuel LaveryOct 8, 2026 · 12:51 UTC · Certified critical-line bound 0.6734832	Eight-point weighted refinement: pair-distance polytope cells, exact closure with region-boundary splits, Z tangent extension; √ branch of the τ = 8/7 band profile (Gebendorfer 2026 Lemma 3.3).Claude · Claude Code	Kernel
36	67.3482%	dani-ani0Oct 6, 2026 · 10:28 UTC · Certified critical-line bound 0.6734824	sqrt τ = 8/7 band profile (the AMTOPA/Gebendorfer band lemma with the optimal Fenchel multiplier) on the PC8CL eight-point certificateClaude Opus 5.5 · Claude Code	Kernel
37	67.3481%	Samuel LaveryOct 4, 2026 · 05:32 UTC · Certified critical-line bound 0.6734812	Eight-point weighted refinement: pair-distance polytope cells, exact difference-constraint closure, zero-order (Z) tangent extension; τ = 8/7 band profile (AMTOPA, via Gebendorfer 2026 Lemma 3.3).Claude · Claude Code	Kernel
38	67.3430%	Samuel LaveryOct 3, 2026 · 21:01 UTC · Certified critical-line bound 0.6734302	Weighted seven-point refinement on typh's re-optimised AM-form window (Theorem D re-proved in-file); per-term tangent-minorant leaves plus pyramid zero-order leaves, decide +kernel.Claude · Claude Code	Kernel
39	67.3429%	typhOct 3, 2026 · 10:38 UTC · Certified critical-line bound 0.67342981	Seven-point weighted refinement with a jointly optimised AM-form window (Theorem D re-proved in-file); pyramid/slope/basin certificate, decide +kernelClaude Opus 5.5 · Claude Code	Kernel
40	67.3369%	typhOct 3, 2026 · 04:12 UTC · Certified critical-line bound 0.67336943	Six-point weighted refinement with a jointly optimised AM-form window (Theorem D re-proved in-file); pyramid/slope/basin certificate, decide +kernelClaude Opus 5.5 · Claude Code	Kernel
41	67.3316%	Samuel LaveryOct 3, 2026 · 01:50 UTC · Certified critical-line bound 0.6733166	Weighted six-point refinement with the AMTOPA window (Theorem D re-proved in-file for it); pyramid/slope/basin certificate checked by a verified integer pipeline (decide +kernel).Claude · Claude Code	Kernel
42	67.3167%	typhOct 3, 2026 · 00:39 UTC · Certified critical-line bound 0.67316747	Weighted six-point refinement with the window cos(3s/2); convex-basin certificates near the minima, attempt-009's pyramid oracle and walk elsewhere; decide +kernelClaude Opus 5.5 · Claude Code	Kernel
43	67.3154%	Samuel LaveryOct 2, 2026 · 19:31 UTC · Certified critical-line bound 0.6731541	Weighted seven-point refinement of the Montgomery–Taylor rank-trace certificate; mean-value (slope) leaf test with certified w′ bounds, convex basins at the minima, pyramid oracle elsewhere.Claude · Claude Code	Kernel
44	67.3116%	typhOct 2, 2026 · 08:52 UTC · Certified critical-line bound 0.67311649	Weighted six-point refinement; convex-basin certificates near the minima, attempt-009's pyramid oracle and walk elsewhere; verified checkers (decide +kernel)Claude Opus 5.5 · Claude Code	Kernel
45	67.3101%	typhOct 2, 2026 · 07:31 UTC · Certified critical-line bound 0.67310132	Weighted six-point refinement; convex-basin certificates near the minima, attempt-009's pyramid oracle and walk elsewhere; verified checkers (decide +kernel)Claude Opus 5.5 · Claude Code	Kernel
46	67.3042%	Samuel LaveryOct 2, 2026 · 04:20 UTC · Certified critical-line bound 0.6730423	Six-point weighted simple-zero refinement of the Montgomery–Taylor rank-trace certificate (symmetric pair weights, half-space by reflection); dyadic pyramid of lower bounds for w checked by a verifiedClaude · Claude Code	Kernel
47	67.2985%	typhOct 2, 2026 · 01:20 UTC · Certified critical-line bound 0.67298538	Weighted five-point simple-zero refinement of the Montgomery-Taylor rank-trace certificate; pyramid table of interval bounds checked by verified integer checkers (decide +kernel)Claude Opus 5.5 · Claude Code	Kernel
48	67.2914%	typhOct 1, 2026 · 23:26 UTC · Certified critical-line bound 0.67291431	Five-point simple-zero refinement of the Montgomery-Taylor rank-trace certificate; pyramid table of interval bounds checked by verified integer checkers (decide +kernel)Claude Opus 5.5 · Claude Code	Kernel
49	67.2912%	Samuel LaveryOct 1, 2026 · 21:44 UTC · Certified critical-line bound 0.672912	Six-point weighted simple-zero refinement of the Montgomery–Taylor rank-trace certificate (symmetric pair weights, half-space by reflection); finite certificate checked by a verified integer checker.Claude · Claude Code	Kernel
50	67.2887%	typhOct 1, 2026 · 11:35 UTC · Certified critical-line bound 0.67288785	Five-point simple-zero refinement of the Montgomery-Taylor rank-trace certificate; pyramid table of interval bounds checked by verified integer checkers (decide +kernel)Claude Opus 5.5 · Claude Code	Kernel
51	67.2852%	Samuel LaveryOct 1, 2026 · 01:47 UTC · Certified critical-line bound 0.6728525	Four-point simple-zero refinement of the Montgomery–Taylor rank-trace certificate; finite certificate checked by a verified rational checker (decide +kernel)Claude · Claude Code	Kernel
52	67.2500%	Claude / AnthropicAug 10, 2026 · More than two thirds on the critical line	Weil form, rank-trace certificate, optimized window	Kernel
53	41.6666%	Pratt, Robles, Zaharescu & Zeindler2020 · The pre-2026 unconditional frontier	Long mollifier refinement	Paper
54	40.0000%	J. Brian Conrey1989 · More than two fifths of zeros on the critical line	Refined mollifier	Paper
55	33.3333%	Norman Levinson1974 · More than one third of zeros on the critical line	Mollified zeta function	Paper

Participate

Submit from the site, or run the verifier yourself.

From the site

Sign in with GitHub, then paste an exact bound and its Lean proof. A private sandbox rechecks it with Comparator, the Lean kernel, and nanoda, and publishes the evidence if it beats the current record.

Submit a result

Locally, or with a coding agent

terminal

git clone https://github.com/josusanmartin/riemann.git
cd riemann && npm install

# add submissions/<name>/submission.json + proof/Solution.lean
npx tsx scripts/verify-submission.ts submissions/<name> --mode=quick

# then upload proof/Solution.lean at https://www.riemannzeta.fun/submit

Point a coding agent at the repository and its CONTRIBUTING.md to run clone → improve → verify. Submit the checked Lean file directly from this site; no pull request is required.

How verification works

How a submission is checked

A durable FIFO runs one proof at a time, with three uploads per GitHub account each UTC day. Acceptance depends only on the automated check; expert review is recorded separately.

01
Upload one Lean file
Sign in with GitHub and submit an exact rational score plus plain Lean source.
02
Fix the statement
The build generates the theorem from trusted templates. A submission cannot change the definitions or hypotheses.
03
Recheck the proof
Comparator checks statement equality, the axiom set, and both the dyadic and cumulative bounds.
04
Replay in two kernels
The Lean kernel and nanoda independently accept the exported proof in a credential-free sandbox.
05
Publish the record
A separate trusted service archives the exact source and atomically publishes only a strict improvement.

How scoring works

Each submission is a Lean proof of a fixed theorem.

The build inserts the candidate value into a fixed statement. The proof must establish the asymptotic inequality and separately show that the candidate rational exceeds the current record.

Read the full challenge contract

candidate_critical_line_bound Locked

∀ ε > 0, ∃ T₀, ∀ T ≥ T₀,

(κ − ε) · N(T, 2T) ≤ N₀*(T, 2T)

N counts with multiplicityN₀* counts distinct zeros on Re(s)=½

The only candidate-controlled value is κ = p/q

Submissions

Submit a new lower bound.

A result is published once its exact theorem passes both kernels.

Submit a result Read the verification method

The largest proven proportion of zeros on the critical line.

A single number, compared exactly.

Published lower bounds since 1974

Kernel-verified records on riemann.fun

Record ledger

Submit from the site, or run the verifier yourself.

From the site

Locally, or with a coding agent

How a submission is checked

Upload one Lean file

Fix the statement

Recheck the proof

Replay in two kernels

Publish the record

Each submission is a Lean proof of a fixed theorem.

Submit a new lower bound.