Dead ends in square-free digit walks
Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta

TL;DR
This paper investigates the rarity of dead-end square-free digit walks across different bases, providing precise asymptotic densities and formal proofs using automated theorem proving tools.
Contribution
It establishes the true asymptotic dead-end density, significantly lower than previous models, and derives a closed-form expression for dead-end densities in all bases, formalized in Lean/Mathlib.
Findings
True dead-end density is approximately 1.317×10^{-9}.
Dead-end densities exist for all bases and are given by a closed-form expression.
The formal proof was generated automatically using AxiomProver.
Abstract
We study "dead ends" in square-free digit walks: square-free integers such that, in base , every one-digit extension is non-square-free. In base , the stochastic independence model of Miller et al. suggests that infinite square-free walks occur with probability near , corresponding to an asymptotic dead-end density of . We prove that the true asymptotic dead-end density satisfies \[ c_{\mathrm{dead}} \approx 1.317\times 10^{-9}, \] roughly a factor of smaller than the prediction. For every base , we prove that dead-end densities exist and are given by a closed-form expression (as a finite alternating sum of Euler products). The argument is fully formalized in Lean/Mathlib, and was produced automatically by AxiomProver from a natural-language statement of the problem.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsStochastic processes and statistical mechanics · Markov Chains and Monte Carlo Methods · Complexity and Algorithms in Graphs
