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 proof in a form that has been formally verified in Lean 4. The argument includes the reduction to colossally abundant integers, the implication under the Riemann hypothesis, the Nicolas–Landau oscillation argument for the converse, and exact certificates for the bounded range. The analytic and arithmetic ingredients are those of Robin and of the authors he cites; the decomposition into explicit lemmas and the finite certificate system are part of the formal reconstruction. The theorem is an equivalence criterion and does not prove the Riemann hypothesis

Keywords