{"id":"palomar/PALOMAR-2026-09-14-000007","url":"https://github.com/kimihiro64/Robin1984/tree/acab1a31f31e0499518a4416b63281e0b4838f9c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-14-000007-v1.json","repo":"https://github.com/kimihiro64/Robin1984","tags":["math.NT","msc:11M26","msc:11N37","msc:03B35","riemann-hypothesis","lean","analytic-number-theory"],"score":0,"title":"Robin1984","trust":"high","domain":"math.NT","source":"palomar","authors":["Jonas Whidden"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 formalization of Guy Robin's 1984 equivalence between the Riemann hypothesis and the strict divisor-sum inequality sigma(n) 5040. The development also proves the restriction to colossally abundant integers, reconstructs the Nicolas--Landau oscillation argument used for the converse implication, and checks the finite ranges with exact Lean certificates. It also formalizes Lagarias's 2001 elementary harmonic-number criterion and its equivalence to the Riemann hypothesis. This is a formalization of equivalence criteria; it does not prove the Riemann hypothesis.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-14","reactions":{},"formalized":true,"formalizes":[{"title":"Grandes valeurs de la fonction somme des diviseurs et hypothese de Riemann","identifier":"MR0774171","relationship":"formalizes"},{"title":"An Elementary Problem Equivalent to the Riemann Hypothesis","identifier":"https://doi.org/10.1080/00029890.2002.11919883","relationship":"formalizes"},{"title":"Petites valeurs de la fonction d'Euler","identifier":"https://doi.org/10.1016/0022-314X(83)90055-0","relationship":"formalizes"},{"title":"Uber einen Satz von Tschebyschef","identifier":"https://eudml.org/doc/158244","relationship":"formalizes"},{"title":"Estimates for the Chebyshev Function psi(x) - theta(x)","identifier":"https://doi.org/10.2307/2007805","relationship":"formalizes"}]}