A machine-checked Lean 4 formalization of Stokes' theorem on smooth singular cubes with true Fréchet pullback, chain-level extensions, and comparison to prior HOL Light work.
Gouëzel,Smooth manifolds in Lean, contributed tomathlib4; seeMathlib.Geometry.Manifold.SmoothManifoldWithCorners,https:// leanprover-community.github.io/mathlib4_docs/
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
fields
cs.LO 1years
2026 1verdicts
ACCEPT 1representative citing papers
citing papers explorer
-
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
A machine-checked Lean 4 formalization of Stokes' theorem on smooth singular cubes with true Fréchet pullback, chain-level extensions, and comparison to prior HOL Light work.