{"id":"palomar/PALOMAR-2026-10-27-000015","url":"https://github.com/nitromannitol/Random-Walk-On-Sphere-Packings/tree/65f7a1116f889c4943b0bce1df7f5b4b464a13ac","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000015-v1.json","repo":"https://github.com/nitromannitol/Random-Walk-On-Sphere-Packings","tags":["math.PR","msc:60G50","msc:60K37","msc:65M08"],"score":0,"title":"Random walk on sphere packings and Delaunay triangulations in arbitrary dimension","trust":"high","domain":"math.PR","source":"palomar","authors":["Ahmed Bou-Rabee"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 formalization of the paper \"Random walk on sphere packings and Delaunay triangulations in arbitrary dimension\" by Bou-Rabee and Gwynne: on orthogonal tilings with small mesh and one of three regularity hypotheses, the stopped conductance-weighted random walk converges to stopped Brownian motion modulo time parametrization (Theorem A) and the discrete Dirichlet problem converges (Theorem B, both alternatives); Poisson-Voronoi tessellations satisfy the hypotheses (Proposition 1.1); and simple random walk on a bounded-degree sphere packing need not converge (Theorem 6.1); for any…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Random walk on sphere packings and Delaunay triangulations in arbitrary dimension","identifier":"arXiv:2405.11673v2","relationship":"formalizes"}]}