Skip to content
#

zero-axiom

Star

Here is 1 public repository matching this topic...

DavidFox998 / rh-core-c01-c07

Star 0

Lean 4 RH proof chain C01-C21 via Arakelov geometry of X₀(143). 61 files · 0 sorry · 0 axiom · classical trio only · Mathlib v4.12.0. Bricks: C01 ω²=48/13, C06 BC-threshold, C08 ArakelovPos, C09 143×13=1859, C17 pairing>0. Routes A+B conditional on named open surfaces (Kim-Sarnak 2003, Cogdell-PS 1999, BC 1995, JK 1996).

mathlib riemann-hypothesis lean4 formal-proof clay-mathematics arakelov-geometry x0-143 zero-sorry zero-axiom classical-trio kim-sarnak-2003 bost-connes-1995 cogdell-ps-1999 jk-1996 c01-c21 arakelov-pairing-proved p5-bridge-14 conditional-proof-chain
  • Updated Jun 23, 2026
  • Lean

Improve this page

Add a description, image, and links to the zero-axiom topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the zero-axiom topic, visit your repo's landing page and select "manage topics."

Learn more