Mathematics

Riemann Hypothesis: A Lean 4 Formalization

by Travis Darshan · Independent Researcher

Lean 4 formalization made public May 30, 2026 on GitHub  ·  Archived on Zenodo August 15, 2026

The Riemann Hypothesis is one of the oldest and most famous unsolved problems in mathematics. First posed in 1859, it concerns the hidden structure underlying the prime numbers, and for more than a century and a half it has resisted proof.

Travis Darshan's research is presented in two complementary forms: the mathematical manuscript and a large-scale Lean 4 formalization. The manuscript sets out the mathematical framework in conventional form; the Lean development carries that framework into a machine-checkable system, where the formal proof is checked by Lean's kernel. Working independently, outside any university or institution, he has assembled a formal library running to more than 125,000 lines of Lean across over 2,700 verified theorem/lemma declarations.

The Lean 4 formalization is built on the manuscript's core theory, with a few refinements tightened along the way, and an updated manuscript coming.

At the center of that library is a single, carefully stated result: a machine-verified conditional theorem whose endpoint is the full Riemann Hypothesis. The project has not yet closed the Riemann Hypothesis unconditionally. The remaining condition is explicit in the formal development rather than hidden behind an unfinished proof placeholder or a custom axiom. Closing that remaining condition is the project's current research frontier.

Travis Darshan's Lean 4 verification output shows that the certified result builds with no sorry or admit placeholders and no custom axioms. In Lean, a sorry is a placeholder for a step you haven't actually proved — it tells the system to assume the result and move on, so even one buried anywhere leaves a gap in the proof. Having no sorry means nothing in the compiled formalization is skipped with an unfinished proof placeholder; combined with the absence of custom axioms, the certified result rests only on Lean's standard logical foundation.

The repository provides direct instructions for independently reproducing the verification by cloning and running the Lean 4 project yourself. Anyone can re-run the repository's exact verification commands and check the result independently. As of now, Travis Darshan's certified Lean 4 formalization compiles with no sorry. That openness is the point — the work is presented so that its formal results can be carefully examined and independently verified.

What makes the project unusual is the combination: an original mathematical framework carried into a large public Lean 4 formalization, with a kernel-checked Riemann Hypothesis endpoint, zero sorry or admit, no custom axioms, and source files that others can independently inspect, clone, rebuild, and verify.