{"id":"palomar/PALOMAR-2026-09-10-000005","url":"https://github.com/sweeneyde/1mfld/tree/83e961ba28dd8182e7bae844756aba614eb1512e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-10-000005-v1.json","repo":"https://github.com/sweeneyde/1mfld","tags":["math.GT","math.GN","msc:57N99","msc:54F65","msc:68V20","topology","manifolds","lean","formalization"],"score":0,"title":"The classification of compact 1-manifolds","trust":"high","domain":"math.GT","source":"palomar","authors":["Jim Fowler","Dennis Sweeney"],"reviews":0,"subject":"math.GT","summary":"A Lean 4 (mathlib) proof of the classification of 1-manifolds, specifically that every compact, connected, Hausdorff topological space charted on the half-line [0,∞) is homeomorphic to the circle S¹ or to the closed unit interval [0,1]. The proof follows David Gale's outline: shrink to a finite atlas of interval charts, then induct on the atlas size, merging two overlapping charts at each step; a connected overlap glues two charts into one (two boundary charts glue onto [0, 1]), while a disconnected overlap has exactly two components and yields the circle.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-10","reactions":{},"formalized":true,"formalizes":[{"title":"The classification of 1-manifolds: a take-home exam","identifier":"https://doi.org/10.2307/2322421","relationship":"formalizes"}]}