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, Ishan Sinha, Jimmy Xin, Jujian Zhang
math.CO
Feb 4, 2026 · v1
TL;DR
Argument formalized in Lean/Mathlib and produced automatically by AxiomProver from a natural-language statement.
Abstract
We study "dead ends" in square-free digit walks: square-free integers $N$ such that, in base $b$, every one-digit extension $bN+d$ is non-square-free. In base $10$, the stochastic independence model of Miller et al. suggests that infinite square-free walks occur with probability near $1$, corresponding to an asymptotic dead-end density of $\approx 5.218\times 10^{-5}$. We prove that the true asymptotic dead-end density satisfies \[ c_{\mathrm{dead}} \approx 1.317\times 10^{-9}, \] roughly a factor of $\sim 4\times 10^4$ smaller than the prediction. For every base $b\geq 2$, 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.
Problem
The stochastic independence model of Miller et al. predicts an asymptotic dead-end density of approximately 5.218e-5 for square-free digit walks in base 10, but the true density was unknown. Whether dead-end densities exist for all bases and have closed-form expressions was open.
Approach
Dead ends are square-free integers N such that every one-digit extension bN+d is non-square-free. The argument derives a closed-form expression (a finite alternating sum of Euler products) for dead-end densities in every base b >= 2. The proof is fully formalized in Lean/Mathlib and was produced automatically by AxiomProver from a natural-language statement.
Results
The true asymptotic dead-end density in base 10 is approximately 1.317e-9, roughly a factor of 4e4 smaller than the independence-model prediction. Dead-end densities are proved to exist for every base b >= 2.
