{
  "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\\sqrt{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 $\\lceil 2\\sqrt{N} \\rceil$ below $N$. The frontier lemma becomes a certificate: the $\\lceil 2\\sqrt{N} \\rceil$ 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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": "2609.22298",
  "author_total": 2,
  "authors": [
    {
      "name": "Ibrahim Mian"
    },
    {
      "name": "Shayaan Siddique"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/baaztgvekvf0d.bib",
  "cited_by": 0,
  "doi": "10.48550/arxiv.2609.22298",
  "fulltext_url": null,
  "id": "baaztgvekvf0d",
  "issns": [],
  "landing_url": "https://arxiv.org/abs/2609.22298",
  "language": null,
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "http://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": "CC0-1.0",
  "native_subjects": [
    [
      "arxiv",
      "math.GM"
    ],
    [
      "openalex",
      "2602|Analytic Number Theory Research"
    ]
  ],
  "openalex": "W7214018684",
  "pdf_url": "https://arxiv.org/pdf/2609.22298",
  "pmcid": null,
  "pmid": null,
  "published": "2026-09-14",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/baaztgvekvf0d.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:23:27Z",
      "native_id": "2609.22298",
      "source": "arxiv",
      "url": "https://arxiv.org/abs/2609.22298"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "openalex:2602|Analytic Number Theory Research",
      "subfield": "algebra-number-theory"
    }
  ],
  "title": "Kernel-Checked Frontier Certificates for Erdős Problem 414",
  "title_text": "Kernel-Checked Frontier Certificates for Erdős Problem 414",
  "type": "preprint",
  "updated_at": "2026-10-30T12:23:27Z",
  "url": "https://research.draconitic.com/paper/baaztgvekvf0d",
  "venue": "arXiv",
  "versions": []
}