ROBIN’S 1984 CRITERION FOR THE RIEMANN HYPOTHESIS: A FORMALLY VERIFIED PROOF

Abstract

Abstract. Guy Robin proved in 1984 that the Riemann hypothesis is equivalent to the strict inequality σ(n) < eγ n log log n (n > 5040). We give a detailed mathematical reconstruction paired with a formally verified Lean 4 proof. The argument reduces arbitrary integers to colossally abundant extrema, proves the bounded range with exact rational certificates, establishes the large-height implication under the Riemann hypothesis through a weighted explicit formula and a strict coefficient gap, and proves the converse by turning Nicolas–Landau oscillations into least-common-multiple counterexamples. The source-specific weighted formula and oscillation argument are proved in repository-owned modules, while substantial foundational analysis is imported from pinned public libraries: axiom- free here does not mean dependency-free or redeveloped from first principles. A declaration-level map connects the exposition to the checked source. Comparator verifies that the solution proves the exact Mathlib-only challenge statements and respects the configured axiom boundary; Lean’s kernel and the independent NanoDa kernel then replay the export. Public source, certificates, CI logs, release artifacts, and reproduction instructions make this assurance chain inspectable. The reconstruction used a human-directed automated context system to track sources, theorem state, dependencies, numerical evidence, and verification status. The paper documents its role through retained outputs and two concrete failure-and-revision cases, without claiming a measured productivity advantage. Reusable outputs include a generic positive-transform theorem, multiplicity-aware zero infrastructure, and a theorem-parametric finite-certificate checker. Robin’s result remains an equivalence criterion; it does not prove the Riemann hypothesis.

Keywords