Robin1984

Robin1984 is a Lean 4 formalization of Guy Robin's 1984 criterion for the Riemann hypothesis. It proves that

RiemannHypothesis <->
  forall n > 5040, sigma(n) < exp(gamma) * n * log(log n),

and proves the equivalent restriction to colossally abundant integers. The repository also reconstructs the Nicolas--Landau oscillation argument used in the converse implication and discharges the finite ranges with exact, kernel-checked certificates.

It also formalizes Lagarias's 2001 elementary criterion, proving that the Riemann hypothesis is equivalent to sigma(n) <= H_n + exp(H_n) * log(H_n) for every positive integer n.

This is a formalization of an equivalence criterion. It does not prove the Riemann hypothesis.

Advertised results

The small statement surface is Challenge.lean. Palomar Comparator checks the corresponding proved declarations in Solution.lean:

• Robin1984.robin_inequality_iff_riemannHypothesis formalizes Robin's equivalence between the Riemann hypothesis and the strict divisor-sum inequality for every integer n > 5040.
• Robin1984.riemannHypothesis_iff_colossallyAbundant_robin proves that it is equivalent to verify the same inequality on colossally abundant integers above 5040.
• Robin1984.riemann_hypothesis_iff_lagarias_elementary_criterion formalizes Lagarias's elementary criterion in terms of harmonic numbers.

The Challenge definitions use Mathlib's divisor sum, Euler--Mascheroni constant, harmonic numbers, real logarithm and real power, and RiemannHypothesis predicate. There are no hidden hypotheses in any of the three compared theorems.

Mathematical organization

The proof development is organized by mathematical role:

• Robin1984/Arithmetic/ defines Robin's inequality and elementary divisor and logarithmic bounds.
• Robin1984/ColossallyAbundant/ develops marginal prime-power events, colossally abundant threshold profiles, and the reduction to CA integers.
• Robin1984/Finite/ contains the exact startup proof, rational tangent rows, and kernel-checked finite certificates.
• Robin1984/Lagarias/ proves the harmonic comparison, finite range, and the forward and converse bridges for Lagarias's elementary criterion.
• Robin1984/Analytic/ proves the explicit Mertens, prime-power and large-height estimates used under RH.
• Robin1984/NicolasLandau/ reconstructs Nicolas's oscillation argument and Landau's positive-transform principle, including the weighted explicit formula and multiplicity-aware xi-zero sums.
• Robin1984/Equivalence/ assembles the finite and analytic implications into the public equivalence theorem.
• Robin1984/Helpers/ contains reusable event, threshold, state and prime-tower lemmas.
• Robin1984/Mathlib/ contains project-independent modules maintained in their proposed upstream namespaces and source format.

The finite proof has three visible parts. Exact prime factorizations cover 5041 <= n < 7560; a common colossally abundant tangent covers 7560 <= n < 720720; and 36 rational log-height rows cover the remaining finite range through log n = 74500. The final retained row uses 105 bounded prime-product blocks, each recomputed with decide +kernel.

Mathlib candidate layer

MATHLIB_PORTING.md inventories the reusable modules maintained for possible upstreaming. The current candidate layer contains nine modules covering Abel identities, Nat.lcmUpto support, finite Mertens products, exact rational logarithm bounds, one-sided Omega transfer, absolute tail reweighting, nonnegative-MGF continuation, and positive-real zeta nonvanishing. Each uses its proposed upstream namespace at a path mirroring its intended Mathlib destination. Existing project declarations and the advertised downstream API retain their original names.

The import audit enforces a one-way boundary: candidates may depend only on narrow Mathlib-family modules or other candidates, never on Robin1984 proof code or third-party project libraries. It also checks Mathlib source headers, absence of the project namespace from candidate bodies, one manifest row per candidate, and a recognized readiness state. All nine candidates build directly against the pinned Mathlib revision before the complete project.

Provenance

Every project-specific Lean file has two separate module headers:

1. a content-reviewed provenance designation identifying whether the file directly formalizes Robin, Nicolas, Landau or another published source; records a standard mathematical formalization; or is primarily original to this Lean development; and
2. a human-readable description of the module's definitions, theorems and role in the proof.

Mathlib candidate source instead uses Mathlib's upstream-ready copyright, licence, authorship and module-documentation header while retaining an exact reviewed entry in the repository provenance ledger.

The review methodology and category counts are in docs/PROVENANCE.md. The machine-readable, path-exact review record is provenance/ledger.json. Provenance was assigned from the contents and dependency role of each file, not from filename or keyword matching.

Primary mathematical references include:

• Jeffrey C. Lagarias, An Elementary Problem Equivalent to the Riemann Hypothesis, American Mathematical Monthly 109 (2002), 534--543; submitted in 2001.
• Guy Robin, Grandes valeurs de la fonction somme des diviseurs et hypothese de Riemann, Journal de Mathematiques Pures et Appliquees 63 (1984), 187--213.
• Jean-Louis Nicolas, Petites valeurs de la fonction d'Euler, Journal of Number Theory 17 (1983), 375--388.
• Edmund Landau, Uber einen Satz von Tschebyschef, Mathematische Annalen 61 (1905), 527--550.
• N. Costa Pereira, Estimates for the Chebyshev function psi(x)-theta(x), Mathematics of Computation 44 (1985), 211--221, with the 1987 corrigendum.

The complete structured bibliography and source relationships are recorded in formalization.yaml. The accompanying research paper presents the mathematical proof, theorem-by-theorem correspondence, and original references.

Trust and proof surface

The completed kernel axiom audit of the three proved Solution declarations returned exactly Lean's standard principles propext, Classical.choice, and Quot.sound. Project proof sources contain no custom axiom declarations, sorry, admit, or native_decide. The three deliberate sorrys in Challenge.lean are statement holes required by the Challenge/Solution comparison and are excluded from proof-status counts.

Finite certificates use ordinary decide +kernel, exact natural and rational arithmetic, and proved soundness theorems. Comparator statement checking and an independent NanoDa replay are configured as release gates in Linux CI.

Lean version and dependencies

The project is pinned to Lean v4.33.1; see lean-toolchain and lake-manifest.json. The proof depends on Mathlib and leancert at pinned Git revisions. The analytic dependency PrimeNumberTheoremAnd is fetched from a temporary public compatibility and extension fork at the exact commit recorded in the manifest. That commit is based on upstream commit 47fa48680663df41146704d02a5b092d792bd5b9 and contains the Lean 4.33.1 proof repairs plus the xi-divisor and Mertens interfaces used here. As of September 2026, upstream main still declares Lean 4.32.2 and does not contain the required xi-divisor source. The fork can be removed after a compatible upstream revision contains or replaces those interfaces and the full build and Comparator/NanoDa checks pass. The added xi-divisor source retains Matteo Cipollina's authorship and Apache-2.0 notice. A fresh Lake build reconstructs the dependency from public Git history and needs no local or build-time patch step.

Building

Install Git and elan, then ensure the pinned toolchain can be installed. On Windows PowerShell:

./scripts/bootstrap.ps1
lake exe cache get
lake build

On Linux or macOS:

lake update
lake exe cache get
lake build

The bare lake build command is the complete submission build. Its default targets are Challenge and Solution; they use Lake's ordinary scheduler, so unrelated modules can build concurrently. The memory-intensive Robin and Lagarias certificate modules encode their order as import-dependency ladders, keeping those elaborations sequential in both repository and consumer builds. Each Lean process is additionally bounded to one internal task thread (-j1).

The finite certificates are deliberately substantial, so a fully uncached build is dominated by their kernel reductions and can take considerably longer than an incremental replay. It needs several GiB of free disk space and adequate memory; no machine-independent cold-build duration is claimed.

Checks

The repository's local checks are:

./scripts/check-imports.ps1
./scripts/check-provenance.ps1
ruby ./scripts/validate-formalization.rb

The import linter rejects package and Mathlib-category umbrella imports, duplicate or unresolved imports, non-canonical header ordering, and local imports already supplied transitively by another direct import. It also enforces the Mathlib candidate boundary and inventory. The subsequent Lean build separately verifies that every retained narrow import provides the notation, tactics, instances, and declarations its file actually needs.

On a Linux host with Git, Lake, Go, Rust/Cargo, Python 3 and Landrun support, run the pinned Comparator and NanoDa toolchain with:

./scripts/verify-comparator.sh

The verifier first runs the repository's sequential default build. Comparator then exports the Challenge and Solution environments separately, compares each advertised theorem statement and the declarations used by that statement, audits the Solution proof bodies against the three permitted standard axioms, and replays the export through Lean's default kernel. The configuration has no definition holes and requires a second replay through the independent NanoDa kernel. Linux CI passes the completed root .lake/build tree from its build job to the documentation and Comparator jobs, avoiding redundant concurrent cold builds while retaining the same checks on fresh standalone verifiers. It pins the upstream leanprover/lean4export v4.33.0 source commit and compiles that source unmodified with this repository's exact Lean v4.33.1 toolchain via ELAN_TOOLCHAIN. This keeps the exporter compatible with the project's .olean format without a fork or a machine-local patch. The build job also caches that tree across workflow runs under a key derived from every Lean source and build-defining file. A source change therefore forces a new kernel build, while documentation-only changes can reuse the exact Linux .oleans.

API documentation is checked by the Linux CI job and can be built from the nested docbuild project on a host with a compatible native C toolchain:

cd docbuild
lake build Robin1984:docs

doc-gen4 includes every transitive import so that declaration links resolve. The project therefore avoids umbrella import Mathlib declarations and CI caches docbuild/.lake/build, allowing later documentation runs to update the existing database rather than regenerate every imported module. After doc-gen4 finishes, CI replaces its server-oriented root page with the committed offline landing page and checks every link before uploading the site. The resulting index.html works when the documentation archive is opened directly after extraction, without a web server, iframe, external script or CDN.

The same CI run publishes the compiled research paper as the robin1984-research-paper artifact. Its cached PDF is keyed only by paper/robin1984-formalization.tex, so an unchanged paper source reuses the same PDF instead of rebuilding it. The build uses the source file's last Git change time as SOURCE_DATE_EPOCH and checks that the final PDF is nonempty and has resolved references and a positive page count.

Successful main builds publish an official GitHub release only after every job has passed, including Comparator statement matching, NanoDa replay and Lean's default-kernel replay. The committed RELEASE_VERSION file supplies the semantic version and must be bumped before a new release; CI checks tag collisions before starting the long Lean build. The release contains exactly the paper PDF, a compressed Ubuntu .lake/build tree, and a ZIP of the complete offline-safe API site. The build archive includes the project's licensing statement, while the documentation ZIP also includes the licence and notice files for Lean and every pinned dependency represented in the generated pages. A rerun at an already published commit verifies the existing release instead of creating a duplicate.

Production and review disclosure

The maintainer selected the mathematical goals, source correspondences and public theorem statements. OpenAI Codex agents assisted with Lean proof development, dependency analysis, refactoring, certificate organization, documentation and mechanical audits. Lean's kernel and the independent Comparator/NanoDa pipeline are correctness gates; they are not substitutes for independent expert mathematical review. No such expert review is claimed.

Licence and submission

The repository's original material is licensed under the Apache License 2.0 by default. The research paper is additionally available under CC-BY-4.0, at the recipient's option. Mathematical provenance, cited papers, external dependencies, file-specific exceptions, and generated release archives are explained in LICENSING.md; the project licence does not relicense third-party material or claim ownership of the underlying mathematical results.

Machine-readable citation information for this formalization is provided in CITATION.cff. The canonical source repository is kimihiro64/Robin1984.

Palomar reviews a fixed commit from a public GitHub repository, identified by its full 40-character SHA. See the current submission instructions and use the Palomar submission form only after all checks pass and the exact commit has been pushed.