{"id":"palomar/PALOMAR-2026-08-29-000011","url":"https://github.com/mccorvie/classification-of-surfaces/tree/e3c7230fe78d7b056a415d9ecae6f77887046b32/LeanEval/topological_classification_of_surfaces","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000011-v1.json","repo":"https://github.com/mccorvie/classification-of-surfaces","tags":["math.GT","msc:57K20","topology","surfaces","lean-formalization","classification"],"score":0,"title":"mccorvie/classification-of-surfaces","trust":"high","domain":"math.GT","source":"palomar","authors":["Ryan McCorvie","Jack McCarthy"],"reviews":0,"subject":"math.GT","summary":"A Lean 4 formalization of the classification theorem for compact connected topological 2-manifolds, including surfaces with boundary. The main theorem proves that every compact connected Hausdorff 2-manifold modeled on the Euclidean half-plane is homeomorphic to the sphere, an orientable canonical quotient surface, or a non-orientable canonical quotient surface. The submitted theorem is the exact statement of the Lean Eval `topological_classification_of_surfaces` challenge.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","reactions":{},"formalized":true,"formalizes":[{"title":"Topological classification of surfaces","identifier":"https://lean-lang.org/eval/problems/topological_classification_of_surfaces/","relationship":"formalizes"},{"title":"A Guide to the Classification Theorem for Compact Surfaces","identifier":"https://doi.org/10.1007/978-3-642-34364-3","relationship":"adapts"},{"title":"Geometric Topology in Dimensions 2 and 3","identifier":"https://doi.org/10.1007/978-1-4612-9906-6","relationship":"adapts"}]}