{"id":"hexagon/2609.00152","pdf":"https://hexagonmath.org/pdf/2609.00152v1","url":"https://hexagonmath.org/abs/2609.00152v1","tags":["math.CT","msc:55Q05","msc:18B40","msc:68V20","Lean 4","Mathlib","Seifert van Kampen theorem","categorical pushout","fundamental groupoid","open cover"],"score":0,"title":"A Lean Formalization of the Classical Seifert van Kampen Groupoid Theorem","domain":"math.AT","origin":"ai-generated","source":"hexagon","authors":["Arthur","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.AT","summary":"We explain a Lean 4 formalization of the classical Seifert van Kampen theorem for the full fundamental groupoid. For an arbitrary topological space covered by two open subsets, the inclusion-induced square of ordinary continuous-path fundamental groupoids is a pushout in the category of categories. Every point is retained as an object; no basepoint, connectedness, or separation hypothesis is required. The development identifies an auxiliary directed path category for the indiscrete preorder with Mathlib's fundamental groupoid through strictly inverse functors and naturality equalities. It…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"ai_models":["Codex","Codex"],"discussed":0,"published":"2026-09-30","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":true,"formalizations":["https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000004&version=1"],"human_understanding":"some"}