A centrally excited random walk is a random walk on the integer lattice 
whose first departure from each nonzero site has a drift
toward the origin. For 
and 
, it starts at the origin
and, on first leaving 
, moves to 
with probability 
.
Here 
are the coordinate unit vectors and 
is the Euclidean norm.
All other departures use the simple random walk rule.
Bou-Rabee and Peres (2026) proved that the visited set 
after 
steps has an almost-sure spherical limit shape with radius
 |
(1)
|
where 
is the volume of the unit ball.
For each 
and all sufficiently large 
,
 |
(2)
|
where 
.
If 
counts the visits to 
, then
 |
(3)
|
where 
.
Every site is visited infinitely often.
Bou-Rabee and Peres (2026) report using AI assistants for specific mathematical questions and proof checks, while attributing the main ideas to the authors. They provide a Lean formalization, which has not been independently run here.
