Erdős Problem #367: formalized results

Lean 4 / Mathlib formalizations accompanying the paper Powerful parts of consecutive integers and Davenport–Zannier polynomials (S. D. Hughes).

For an integer n and r ≥ 2, write B_r(n) = ∏_{p^a ∥ n, a ≥ r} p^a for the r-full part of n. Erdős Problem #367 (Erdős–Graham 1980, p. 68; see erdosproblems.com/367) concerns upper and lower bounds for products of powerful parts of consecutive integers.

Contents

Module	Main statement	Paper	Hypotheses
K3AbcUpperBound	erdos_367_k3: abc ⟹ B₂(n)B₂(n+1)B₂(n+2) ≤ C·n^{2+ε}	Thm 1.4 (k=3)	ABCConjecture explicit
GeneralKUpperBound	B2_upper_bound: radical bound RadLB k ⟹ B₂(∏(n+i)) ≤ C·n^{2+ε}	Thm 1.4	RadLB k explicit (a Granville–Langevin consequence of abc)
RFullLowerBound	erdos367_iv: for odd r, n = (q^r−1)^r gives n^{r+1} < (B_r(n)·B_r(n+1))^r	Thm 1.1 (odd case)	unconditional
PellLimsup	erdos367: ∀ M ∃ n, B₂(n)B₂(n+1)B₂(n+2) > M·n²·log n	Thm 1.2 (limsup form)	unconditional
Core139	T1–T3: the E₃ ≥ 13/9 arithmetic core	§3 remark	prime-supply data explicit
Core4027	IDENT: G³ + N³ = H·C³ (degree 27); T1–T3: the E₃ ≥ 40/27 core	Thm 1.3, §5.3	prime-supply data explicit

"Hypotheses explicit" means the named conjecture or the Schur–Hensel prime-supply data appears as a hypothesis of the formal statement; the supply itself and the analytic limsup bookkeeping for the ladder are proved in the paper, not in Lean. The statement erdos367 in PellLimsup is unconditional and self-contained, including the Dirichlet-theorem input.

Verifying

lake exe cache get
lake build

Toolchain: leanprover/lean4:v4.28.0, Mathlib pinned in lake-manifest.json. The build compiles every module with zero sorry and prints an axiom report (Erdos367/AxiomAudit.lean): each theorem above depends only on propext, Classical.choice, Quot.sound — and Core4027.IDENT on propext alone. No native_decide is used.

Relation to the certified sources

The module files are the verification artifacts as produced, with two mechanical changes only: scratch #print axioms lines were removed (the audit now lives in AxiomAudit.lean), and four modules were wrapped in namespaces (GeneralK, RFullOdd, Core139, Core4027) to avoid top-level name collisions when built as a single library.