Dead ends in square-free digit walks

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 $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.