Erdős Problem #520 — resolved in the negative in Lean 4

This repository contains a premise-free, kernel-checked Lean 4 proof that the answer to Erdős Problem #520 is no. Its public theorems use no assumptions beyond Lean's standard foundations (propext, Classical.choice, and Quot.sound), as verified by #print axioms. For the squarefree Rademacher random multiplicative function, Erdős's proposed law-of-the-iterated-logarithm normalization is too large: the normalized partial sums converge almost surely to zero.

The problem

Independently assign a fair sign f(p) ∈ {−1, 1} to every prime p. Extend these signs multiplicatively to squarefree integers and set f(n) = 0 when n is not squarefree. Writing

M_f(N) = Σ_{n ≤ N} f(n),

Erdős asked whether there is a constant c > 0 such that, almost surely,

limsup_{N → ∞} M_f(N) / sqrt(N log log N) = c.

The result

Lean proves the stronger quantitative upper bound: for every η > 0, almost surely there is a constant C ≥ 0 such that, for all sufficiently large N,

|M_f(N)| ≤ C sqrt(N) (log log N)^(1/4 + η).

This is the theorem criticalUpperBound_unconditional. Taking, for example, η = 1/8 makes the exponent 3/8 < 1/2. Dividing by Erdős's scale therefore gives

|M_f(N)| / sqrt(N log log N) → 0

almost surely. In particular, the signed limsup is zero and cannot equal a positive constant.

The public zero-premise endpoints are:

theorem criticalUpperBound_unconditional :
    CriticalUpperBound μ partialSum

theorem erdos520Disproof_unconditional :
    Erdos520Disproof

theorem erdos520NoPositiveConstant_unconditional :
    Erdos520NoPositiveConstant

Thus the answer to Problem #520 is no. This result does not determine whether the exact candidate scale sqrt(N) (log log N)^(1/4) has a finite positive limsup, nor does it prove a matching lower bound. The sharp almost-sure envelope at that scale remains open.

Expository proof note

Release v1.1.0 includes a public note describing the mathematical route, model conventions, formal endpoint statements, axiom audit, and exact prose-to-Lean correspondence:

• Proof note (PDF)
• LaTeX source

The theorem and file links embedded in the PDF are pinned to the v1.1.0 release tag.

Audit the statement first

A proof checker verifies formal statements, so the definitions are deliberately easy to locate:

• Model.lean constructs the product probability space, proves independence of the fair signs, defines the squarefree-supported multiplicative function f, and defines partialSum.
• Basic.lean defines the 1/4 + η critical scale, Erdős's LIL scale, CriticalUpperBound, ZeroLIL, and NoPositiveLILConstant. It also proves deterministically that the critical upper bound implies the zero-LIL conclusion.
• Final.lean identifies the problem-specific propositions Erdos520Disproof and Erdos520NoPositiveConstant with those probability-theoretic statements.
• Unconditional.lean closes every remaining input and exposes the three public theorems above without premises.

The formal partial sum is exactly

partialSum omega N = ∑ k ∈ Finset.range N, f omega (k + 1)

so it runs from 1 through N, matching the stated problem.

Trust audit

The three public endpoints depend only on Lean's standard foundations:

propext, Classical.choice, Quot.sound

There is no sorry, admit, project-specific axiom, assumed published-theorem hypothesis, or external oracle in their dependency chain. The analytic inputs used by the endpoint are proved in Lean, either in this development, in Mathlib, or in the vendored kernel-checked source closures described below.

A literal text search finds axiom qc and axiom hqc inside a documentation example in the vendored AdditiveCombination.lean tactic. They occur inside a block comment, are not Lean declarations, and do not appear in any axiom audit.

To reproduce the audit, elaborate the endpoint file:

lake env lean Erdos/Problem520/Unconditional.lean

The file ends with targeted #print axioms commands for all three public theorems.

Verify the proof

The project is pinned to Lean and Mathlib v4.30.0-rc2; all resolved package revisions are fixed in lake-manifest.json. After installing the tools listed in REQUIREMENTS.md, run:

lake exe cache get
lake build
lake env lean Erdos/Problem520/Unconditional.lean

GitHub Actions performs the same full build and axiom audit on every commit and pull request. Its axiom report is retained as a downloadable workflow artifact. Linter warnings do not affect kernel checking; the build must finish successfully and the final command must report exactly the three standard axioms listed above.

Proof architecture

The formal proof closes the full chain from the random model to the all-integer almost-sure bound:

1. Harper low moment. Euler-product normalization, tilted product laws, Gaussian and ballot comparison, central and moving-height barriers, Parseval, tail control, and local-to-global assembly prove the required low 2/3 moment estimate.
2. Prime inputs. Kernel-checked prime-number-theorem and Selberg-sieve developments supply the scheduled prime-block asymptotics and the uniform Brun–Titchmarsh estimate.
3. Caich reduction. Largest-prime decomposition, smoothing, residual estimates, finite test unions, concentration, and Borel–Cantelli yield the 1/4 + η bound on the selected test mesh.
4. Lau–Tenenbaum–Wu interpolation. A formal fourth-moment mesh argument passes from the test points to every integer.
5. Deterministic endpoint. The 1/4 + η estimate implies convergence to zero at Erdős's sqrt(N log log N) scale.

The names describe the mathematical ancestry of the route. No theorem from the literature is inserted as an unproved premise of the public result.

The active endpoint proves the aligned Caich-style block and residual estimates directly in Lean. The historical conditional thin-block interfaces in Final.lean are retained for comparison, but the unconditional theorem does not use them.

Independent Harper formalization

The central input is itself a premise-free public theorem:

theorem harperRademacherInitialMomentStatement_unconditional :
    HarperRademacherInitialMomentStatement

It proves that there are absolute constants C > 0 and Y ≥ 2 such that, for every y ≥ Y,

E[(2π smoothEnergy(y) / log y)^(2/3)]
  ≤ C / (1 + log log y)^(1/3).

This closes in the kernel the Harper low-moment input consumed by the Caich/Lau–Tenenbaum–Wu part of the argument. Its proof includes the Euler product, tilted law, Gaussian/barrier comparison, central and noncentral moment iterations, Parseval identity, tail estimate, and final weighted assembly. It can be audited independently in HarperUnconditionalInitialMoment.lean.

Repository contents

The repository contains 228 Lean modules covering the complete proof chain, the pinned Lean toolchain and dependency lock, third-party provenance and licenses, citation metadata, the expository proof note, and detailed verification notes.

Citation and license

Machine-readable citation metadata for this formalization is provided in CITATION.cff. The original development is released under the Apache License 2.0; vendored sources retain the upstream notices and licenses recorded in THIRD_PARTY_NOTICES.md. The fixed v1.0.0 archive is identified by 10.5281/zenodo.21782017; the concept DOI always resolves to the latest archived release.

Navigation

• Unconditional.lean: premise-free public conclusions and axiom audits
• HarperUnconditionalInitialMoment.lean: final Harper local-to-global assembly
• HarperCentralEconomicalAssembly.lean: shrinking central bands and terminal core
• HarperUnconditionalFinalAssembly.lean: moving-height noncentral shells and Parseval assembly
• lean_status.md: proof and trust-audit summary
• harper_kernel_route.md: detailed Harper proof route

Vendored sources

Minimal vendored import closures for the prime-number and sieve results live under Erdos/Problem520/External/. Their upstream commits, copyright notices, licenses, and compatibility changes are recorded there and in THIRD_PARTY_NOTICES.md.