The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We formalize this theorem within the framework of computational paths, an approach to equality where witnesses are explicit sequences of rewrites governed by the confluent, terminating LNDEQ-TRS. Our contributions are: (i) pushouts as higher-inductive types with explicit path constructors; (ii) free products and amalgamated free products as quotients of word representations; (iii) an encode-decode proof establishing pi_1(Pushout(A, B, C), f, g) cong pi_1(A) *_{pi_1(C)} pi_1(B); and (iv) applications to the figure-eight (pi_1(S^1 v S^1) cong Z * Z) and 2-sphere (pi_1(S^2) cong 1). The framework makes coherence witnesses explicit as rewrite derivations. The development is formalized in Lean 4, where the pushout axioms and the encode map are assumed, while the decode map, amalgamation compatibility, and applications are fully mechanized (2050 lines). This demonstrates that the encode-decode method for higher-inductive types becomes fully constructive when path equality is decidable via normalization.

翻译：Seifert-van Kampen定理通过空间各组成部分的基本群计算该空间的基本群。我们在计算路径的框架内形式化了该定理，该框架将等式证明视为由合流终止系统LNDEQ-TRS控制的显式重写序列。主要贡献包括：（i）将推出构造定义为具有显式路径构造子的高阶归纳类型；（ii）将自由积与融合自由积定义为词表示形式的商集；（iii）通过编码-解码证明确立 π₁(Pushout(A, B, C), f, g) ≅ π₁(A) *_{π₁(C)} π₁(B) 的同构关系；（iv）应用于八字形空间（π₁(S¹ ∨ S¹) ≅ ℤ * ℤ）与二维球面（π₁(S²) ≅ 1）的计算实例。该框架将一致性证明显式表达为重写推导过程。研究在Lean 4中实现形式化，其中推出公理与编码映射设为公设，而解码映射、融合兼容性及实例应用均实现完全机械化验证（共2050行代码）。这表明当路径等式可通过归一化判定时，针对高阶归纳类型的编码-解码方法具有完全构造性。