Kernel-Checked Frontier Certificates for Erdős Problem 414
Abstract
Let h(n) = n + τ(n), where τ counts divisors. Erdős and Graham asked, after Spiro, whether the orbits of any two positive integers under h eventually share a point (Problem 414 on Bloom's list). The problem is open, and a finite computation cannot close it; nothing about it has been checked by a proof kernel, and the statement in the formal-conjectures repository carries a sorry. We replay what can be certified through the Lean 4 kernel under an axiom gate (axioms exactly propext, Classical.choice, Quot.sound; no sorry; no native_decide). Three elementary facts recorded by Li, namely that coalescence is an equivalence relation, τ(n) is odd exactly for squares, and τ(n) is bounded by 2√n so that orbits skip no square annulus [k2, (k+1)2), are formalized, and his frontier lemma is formalized in a window form: every orbit started below a level N has a point within ⌈ 2√N ⌉ below N. The frontier lemma becomes a certificate: the ⌈ 2√N ⌉ values τ(m) just below N and the orbit points above N until the orbits through the crossing points have merged. Its soundness is a kernel-checked theorem, and the certified rungs state that every pair of positive integers below N coalesces for N = 105, 106, 107, 108; the certificate at 108 has 44,530 entries rather than 108. Every ledger and every quoted count was produced by two programs sharing no code that agree by hash. We record what is known about a non-coalescing pair and measure the exit-set sizes Li bounds. Nothing here is a proof of the conjecture.
Related
- Task-aware Kernel Stein certificates for Rényi differential privacy
- Riesz-energy, finiteness and every-density corollaries of the openai/math planar universal-optimality theorem, kernel-checked in Lean 4
- Planar universal optimality, tiered: kernel-checked consequences, a non-uniqueness theorem, and a CVODE N-body consistency check for the Yukawa interaction
- The Rytova-Keldysh interaction is a positive Gaussian mixture: kernel-checked admissibility for planar universal optimality and Keldysh-jellium Madelung energies of TMD Wigner lattices
- A cutoff-independent enstrophy bound for the sigma = 3 dispersive dyadic shell model: kernel-checked conservation of the second invariant along solutions, CVODE controls, and an illustration on The Well data
BibTeX
@misc{mian2026kernelchecked,
title = {{Kernel-Checked Frontier Certificates for Erdős Problem 414}},
author = {Ibrahim Mian and Shayaan Siddique},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.22298},
eprint = {2609.22298},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.22298},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Kernel-Checked Frontier Certificates for Erdős Problem 414
AU - Ibrahim Mian
AU - Shayaan Siddique
PY - 2026
DA - 2026/09/14
PB - arXiv
DO - 10.48550/arxiv.2609.22298
UR - https://arxiv.org/abs/2609.22298
AB - Let h(n) = n + τ(n), where τ counts divisors. Erdős and Graham asked, after Spiro, whether the orbits of any two positive integers under h eventually share a point (Problem 414 on Bloom's list). The problem is open, and a finite computation cannot close it; nothing about it has been checked by a proof kernel, and the statement in the formal-conjectures repository carries a sorry. We replay what can be certified through the Lean 4 kernel under an axiom gate (axioms exactly propext, Classical.choice, Quot.sound; no sorry; no native_decide). Three elementary facts recorded by Li, namely that coalescence is an equivalence relation, τ(n) is odd exactly for squares, and τ(n) is bounded by 2√n so that orbits skip no square annulus [k^2, (k+1)^2), are formalized, and his frontier lemma is formalized in a window form: every orbit started below a level N has a point within ⌈ 2√N ⌉ below N. The frontier lemma becomes a certificate: the ⌈ 2√N ⌉ values τ(m) just below N and the orbit points above N until the orbits through the crossing points have merged. Its soundness is a kernel-checked theorem, and the certified rungs state that every pair of positive integers below N coalesces for N = 10^5, 10^6, 10^7, 10^8; the certificate at 10^8 has 44,530 entries rather than 10^8. Every ledger and every quoted count was produced by two programs sharing no code that agree by hash. We record what is known about a non-coalescing pair and measure the exit-set sizes Li bounds. Nothing here is a proof of the conjecture.
ER -