We present a sorry-free Lean 4/mathlib4 formalization of Stokes' theorem for smooth singular cubes in arbitrary dimension, using true differential-form pullback via the Frechet derivative. The development also includes a bridge to mathlib4's abstract extDeriv, chain-level Stokes extended by Z-linearity, d^2=0 for singular cubical chains, box Stokes for axis-aligned cubes, dimensional specializations, and a structured comparison with Harrison's HOL Light formalization.

翻译：摘要：我们给出一个无抱歉（sorry-free）的Lean 4/mathlib4形式化证明，针对任意维光滑奇异方体的斯托克斯定理，采用通过弗雷歇导数实现的真微分形式拉回。该形式化体系还包括：通往mathlib4抽象外导数（extDeriv）的桥梁、通过Z-线性扩张的链复形层面斯托克斯定理、奇异立方链的d²=0性质、轴对齐方体的盒状斯托克斯定理、维度特化，以及与Harrison的HOL Light形式化证明的结构化对比。