Let A be the smallest set of positive integers containing 2 and 3 and closed under ab-1 for distinct a, b in A. Erdős, attributing the question to Hofstadter, asked whether A has positive lower density (Erdős Problem 424).

Compositions of the maps T_a(x)=ax-1 are encoded as paths through a finite partition of an interval into 19 subintervals. Transition probabilities are chosen so that the probability of a path equals the reciprocal of the slope of the corresponding affine map. Switching among four multiplier assignments keeps the exponents of 2, 3, 5 and 7 in balance, giving a positive recurrent Markov chain whose returns have slope q^m. The arithmetic renewal theorem then yields on the order of q^m distinct affine maps with slope q^m, which are evaluated at the seed 17.

A has positive lower density: |A ∩ [1,x]| ≥ cx for some c>0 and all sufficiently large x. The proof was formalized in Lean 4, credited in the acknowledgments to Alexeev and Codex.