{"id":"palomar/PALOMAR-2026-10-16-000006","url":"https://github.com/adbrw/HS_proof/tree/b75523f0036bc857f31620ee18af970151036311","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000006-v1.json","repo":"https://github.com/adbrw/HS_proof","tags":["math.GT","math.GR","msc:57S10","msc:22E15","msc:57N65","topological-groups","hilbert-smith","formal-verification","lean"],"score":0,"title":"Hilbert–Smith and p-adic exclusion with second countability","trust":"high","domain":"math.GT","source":"palomar","authors":["adbrw"],"reviews":0,"subject":"math.GT","summary":"A Lean formalization of the Hilbert–Smith statement for a second-countable locally compact Hausdorff topological group acting continuously and faithfully on a connected, Hausdorff, second-countable, finite-dimensional topological manifold. The conclusion gives a smooth real Lie-group structure for the group's existing topology. The development also proves p-adic exclusion for second-countable manifolds and provides universe-polymorphic versions. No second-countability hypothesis is dropped.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Integral tail signatures and the Hilbert–Smith conjecture","identifier":"https://github.com/adbrw/HS_proof/blob/5dee3407a627f35a2cdeb0a34ac9e0f1ee98f862/HSproof.pdf","relationship":"formalizes"}]}