Dead ends in square-free digit walks

Technical Summary: Dead Ends in Square-Free Digit Walks

Problem Statement
The paper investigates the existence and density of "dead ends" in square-free digit walks. A square-free walk in base $b$ begins with a square-free integer $N_0$ and attempts to construct an infinite sequence $N_0, N_1, N_2, \dots$ where each subsequent term is formed by appending a digit $d \in \{0, \dots, b-1\}$ such that $N_{k+1} = bN_k + d$ remains square-free.

A positive integer $N$ is defined as a dead end if:

1. $N$ is square-free.
2. For every digit $d$ in the base, the extension $bN + d$ is not square-free.

The central question, posed by Miller et al. [5], is whether infinite square-free walks exist. While a stochastic model (the "Blind Unlimited Model") suggests that infinite walks exist with probability near 1 (implying dead ends are rare, with an asymptotic density of $\approx 5.218 \times 10^{-5}$ in base 10), this paper rigorously analyzes the actual arithmetic density of dead ends to determine if the stochastic prediction holds.

Methodology
The authors employ a combination of elementary multiplicative number theory and inclusion-exclusion principles, avoiding the probabilistic assumptions of the stochastic model.

1. Indicator Functions: The problem is reformulated using the Möbius function $\mu(n)$. Since $\mu(n)^2$ is the indicator function for square-free integers, the indicator for a dead end $N$ is expressed as:
   $$\mathbb{1}_{N \text{ is dead end}} = \mu(N)^2 \prod_{d \in D} (1 - \mu(bN + d)^2)$$
   where $D$ is the set of digits.

2. Inclusion-Exclusion: The product term is expanded into a sum over all subsets $S$ of the digit set. This transforms the counting function $D_b(X)$ (the number of dead ends $\le X$) into an alternating sum of counting functions $Q_S(X)$, where $Q_S(X)$ counts integers $n \le X$ such that $n$ and all extensions $bn+d$ (for $d \in S$) are square-free.

3. Sieve Analysis: For a fixed subset $S$, the condition that $n$ and $bn+d$ are square-free is analyzed prime-by-prime. The authors define "bad" residue classes modulo $p^2$ that must be avoided. Using the Chinese Remainder Theorem, they determine the density of integers avoiding these classes.

   • For large primes $p$ (where $p \nmid b$), the condition $p^2 \mid (bn+d)$ forces $n$ into a single residue class modulo $p^2$. Crucially, a single prime square can obstruct at most one digit extension at a time.
   • The density is expressed as an infinite product (Euler product) of local factors $(1 - \nu_{p,b}(S)/p^2)$, where $\nu_{p,b}(S)$ counts the number of forbidden residue classes modulo $p^2$.

4. Error Term Control: The proof carefully bounds the error terms arising from truncating the sieve at a parameter $z$ and from the contribution of large primes, establishing an error term of $O(X/\sqrt{\log X})$.

Key Results

• Theorem 1.1 (Base 10): The asymptotic density of dead ends in base 10 exists and is given by:
  $$c_{\text{dead}} = \sum_{S \subseteq \{0,\dots,9\}} (-1)^{|S|} \prod_{p \text{ prime}} \left( 1 - \frac{\nu_p(S)}{p^2} \right)$$
  where $\nu_p(S)$ is the count of residue classes $n \pmod{p^2}$ such that $p^2 \mid n$ or $p^2 \mid (10n+d)$ for some $d \in S$.
  The calculated value is $c_{\text{dead}} \approx 1.317 \times 10^{-9}$.

• Theorem 1.2 (General Base $b$): The result generalizes to any base $b \ge 2$. The density $c_{\text{dead}}(b)$ is given by a similar closed-form expression involving an alternating sum of Euler products. The paper provides computed approximations for prime bases $b \in \{2, 3, 5, 7\}$.

• Discrepancy with Stochastic Models: The true density ($\approx 1.3 \times 10^{-9}$) is roughly $40,000$ times smaller than the stochastic prediction ($\approx 5.2 \times 10^{-5}$). The paper attributes this to arithmetic dependencies: the naive stochastic model assumes independence between digit extensions, but in reality, the requirement that all ten extensions fail simultaneously requires the simultaneous obstruction by many distinct prime squares, a condition much stricter than the independent probability model suggests.

Significance and Claims

• Resolution of Conjecture: The paper demonstrates that while the stochastic heuristic predicts infinite walks are almost certain, the actual arithmetic structure makes dead ends significantly rarer than predicted. However, the existence of an infinite walk remains an open problem; the paper quantifies the rarity of the "obstructions" (dead ends) but does not prove the existence of an infinite path.
• Formalization: A primary claim of the paper is that the main theorem (Theorem 1.2) was fully formalized in Lean/Mathlib and the proof was produced automatically by an AI tool named AxiomProver. The system was provided only with a natural-language statement of the problem and autonomously derived the closed-form formula and the proof.
• Historical Context (Update): The authors note that after the initial arXiv posting, they learned from Kannan Soundararajan that the main result was previously obtained by Mirsky in 1947 [6]. The paper acknowledges that the 2024 work by Miller et al. [5] failed to reference this prior work. Consequently, while the Lean formalization stands as a valid automated proof, the authors state the manuscript will not be submitted for journal publication as a primary research contribution, serving instead as a case study for automated theorem proving.

Conclusion
The paper provides a rigorous arithmetic derivation of the density of dead ends in square-free digit walks, revealing a massive deviation from stochastic predictions due to number-theoretic dependencies. Its most novel contribution, as framed by the authors, is the successful end-to-end automated formalization of this result using AxiomProver, demonstrating the capability of current AI systems to handle non-trivial problems in analytic number theory.