Lean 4 formalization of Robin's 1984 equivalence between the Riemann hypothesis and the divisor-sum inequality above 5040.
theorem-proving number-theory palomar riemann-hypothesis lean4 formalized-mathematics robin-inequality
-
Updated
Sep 12, 2026 - Lean