The divergence theorem and Cauchy integral formula are central results in analysis that lack formal proofs in Lean under minimal regularity assumptions. Standard formulations require regularity of individual partial derivatives, which is unnecessarily restrictive.

The authors formalize a version of the divergence theorem for functions on rectangular boxes that requires only Frechet differentiability and integrability of the divergence, not regularity of individual partial derivatives. The main tool is the GP-integral (a Henstock-Kurzweil variant introduced by Mawhin in 1981). This theorem is then used to prove the Cauchy-Goursat theorem for simple domains and bootstrap complex analysis in Lean's Mathlib.

The formalization provides the divergence theorem under weak regularity assumptions and derives the Cauchy-Goursat theorem and Cauchy integral formula as consequences, contributing foundational complex analysis infrastructure to the Lean mathematical library.