{"id":"palomar/PALOMAR-2026-10-09-000008","url":"https://github.com/laurentbartholdi/whitehead/tree/e0683c947a3120af725ac7a29fc95a059798b64e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-09-000008-v1.json","repo":"https://github.com/laurentbartholdi/whitehead","tags":["math.GT","math.GR","msc:55P15","group-theory","homotopy-theory","asphericity","lean"],"score":0,"title":"Finite Chains of Two-Complexes and Acyclic Covers","trust":"high","domain":"math.GT","source":"palomar","authors":["Laurent Bartholdi","Roman Mikhailov"],"reviews":0,"subject":"math.GT","summary":"Whitehead's asphericity problem would have a negative answer if a non-aspherical two-complex began an infinite chain whose inclusions induce zero maps on second homotopy groups. This Lean formalization proves the article's main finite-length characterization: a connected two-complex K begins such chains of every finite length if and only if K has a connected acyclic regular cover. It also formalizes the finite acyclic enhancement.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-09","reactions":{},"formalized":true,"formalizes":[{"title":"Finite Chains of Two-Complexes and Acyclic Covers","identifier":"arXiv:2610.10074","relationship":"formalizes"}]}