{"id":"palomar/PALOMAR-2026-11-04-000011","url":"https://github.com/scottnarmstrong/elboim-sly/tree/3191c5f9c55c0662ee0bc92b8c79ff27f22f7d46","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-04-000011-v1.json","repo":"https://github.com/scottnarmstrong/elboim-sly","tags":["math.PR","math-ph","msc:60K35","msc:82B20","msc:60G50","msc:60J65"],"score":0,"title":"Infinite cycles in the interchange process in five dimensions (Elboim-Sly), formalized in Lean 4","trust":"high","domain":"math.PR","source":"palomar","authors":["Scott Armstrong","Ahmed Bou-Rabee"],"reviews":0,"subject":"math.PR","summary":"A complete Lean 4 formalization of D. Elboim and A. Sly, Infinite cycles in the interchange process in five dimensions (arXiv:2211.17023v3). In the interchange process on Z^d, each edge carries an independent rate-one Poisson clock and swaps the particles at its endpoints when it rings; run for time beta, it yields a random permutation pi_beta of Z^d. Toth conjectured that pi_beta has infinite cycles for d >= 3 and beta large; Elboim and Sly proved this for d >= 5. The library proves their Theorem 1 (for d >= 5 and beta large, pi_beta almost surely has an infinite cycle), the quantitative…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-04","reactions":{},"formalized":true,"formalizes":[{"title":"Infinite cycles in the interchange process in five dimensions","identifier":"","relationship":"formalizes"}]}