🔢 mathematics

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0

This paper presents a comprehensive, sorry-free Lean 4 formalization of Stokes' theorem for smooth singular cubes using true differential-form pullbacks, while establishing bridges to mathlib4, verifying chain-level properties like $d^2=0$ , and comparing the implementation with Harrison's HOL Light formalization.

Original authors: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Published 2026-05-05

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you have a very complex, multi-dimensional shape, like a crumpled piece of paper or a twisted ribbon floating in space. In mathematics, there is a famous rule called Stokes' Theorem. Think of it as a universal "accounting rule" for shapes. It says that if you want to know the total "activity" happening inside a shape (like the total wind swirling inside a tornado), you don't need to measure every single point inside. Instead, you only need to measure the "edge" or the "boundary" of that shape. The sum of all the activity on the edge perfectly equals the total activity inside.

For a long time, computers (specifically a program called Lean 4) had not been able to prove this rule for every possible shape, especially the weird, crumpled ones that mathematicians call "singular cubes."

This paper is a report on how three researchers finally taught the computer to prove this rule for those tricky shapes, without making any mistakes or skipping steps.

Here is a breakdown of what they did, using simple analogies:

1. The Goal: The "Edge vs. Inside" Rule

Imagine you are painting a room. Stokes' Theorem is like a magic trick that says: "If you know exactly how much paint dripped off the walls (the boundary), you automatically know exactly how much paint was used to cover the whole room (the interior)."

The researchers wanted to prove this trick works even if the "room" is a weird, stretched-out shape defined by a smooth, twisting map (like a rubber sheet being pulled and twisted).

2. The Three-Step Magic Trick

The computer couldn't just "see" the whole shape at once, so the researchers broke the proof down into three logical steps, like a recipe:

Step 1: The "Translation" (Pullback)
Imagine you have a map of a city, but the city is distorted. The researchers created a tool to "translate" the math from the distorted shape back to a perfect, standard cube (like a perfect die). They used a specific mathematical tool called a "pullback" (which is like a high-tech photocopier that copies the rules of the shape onto a standard grid).
Step 2: The "Standard Box" Rule
Once the shape was translated onto a perfect cube, they could use a simpler, already-known rule that works for perfect boxes. They proved that the "inside activity" on this perfect cube equals the "edge activity" on the perfect cube.
Step 3: The "Face Matching"
Finally, they had to prove that the edges of the perfect cube (the translated version) matched up perfectly with the edges of the original, weird shape. They showed that when you add up the edges of the weird shape, they cancel out and line up exactly with the edges of the perfect cube.

3. The "Chain" Connection

The researchers didn't just prove it for one shape. They proved it for a whole "chain" of shapes stuck together.

The Analogy: Imagine building a wall out of bricks. If you put two bricks together, the edge where they touch disappears because it's inside the wall. The researchers proved that if you have a chain of these shapes, the "inner" edges always cancel each other out, leaving only the outer boundary. This is a fundamental rule in math called $\partial^2 = 0$ (the boundary of a boundary is nothing). They proved this by showing that for every time an edge appears, it appears twice with opposite signs, effectively erasing itself.

4. Why This Matters (In the Computer's World)

No "Sorry" Allowed: In computer proof systems, programmers sometimes write "sorry" to say, "I know this is true, but I haven't proved it yet." This paper is special because it has zero "sorry" statements. The computer checked every single step and found no errors.
The Bridge: The researchers built a "bridge" between two different ways of doing math in the computer. One way uses simple coordinates (like a spreadsheet), and the other uses abstract, fancy definitions. They proved that both ways lead to the exact same answer, ensuring the computer isn't just guessing.
Real Smoothness: They required the shapes to be "globally smooth," meaning they are perfectly smooth everywhere, not just in the middle. This made the math easier for the computer to handle, even though it's a stricter rule than what humans usually need.

5. What It Is NOT

The paper is very honest about its limits:

It does not prove this for every possible shape in the universe (like a shape with a sharp corner or a hole that changes size).
It does not deal with "manifolds" (curved surfaces like the surface of a sphere) in the full, complex way mathematicians usually do. It sticks to shapes that can be mapped from a standard cube.
It is a mathematical proof, not a physics experiment. It doesn't predict weather or design bridges; it simply proves that the logical rules of calculus hold up when checked by a computer.

Summary

In short, this paper is a victory for mathematical precision. The researchers taught a computer to verify a 200-year-old calculus rule for a wide variety of twisted, multi-dimensional shapes. They did it by translating the problem into a standard box, proving the rule there, and then showing that the translation was perfect. The result is a "zero-error" proof that the "inside equals the edge" rule works, even for the most complicated smooth shapes we can imagine.

Technical Summary: Stokes' Theorem for Smooth Singular Cubes in Lean 4

Problem Statement
As of April 2026, the Lean 4 ecosystem (specifically mathlib4) lacked a complete formalization of Stokes' theorem for differential forms on smooth manifolds with boundary or for singular chains. While mathlib4 possessed the divergence theorem for axis-aligned boxes and an abstract exterior derivative (extDeriv), it did not yet provide a theorem integrating the pullback of a differential form over a smooth singular cube (a smooth map from a unit cube to an arbitrary Euclidean space) and equating it to the alternating sum of integrals over the boundary faces. Existing formalizations, such as Harrison's work in HOL Light, covered convex and polyhedral domains but did not address smooth singular parametrizations or the specific infrastructure of mathlib4's abstract exterior algebra.

Methodology
The authors present a "sorry-free" formalization (zero unproven assumptions) that bridges the gap between coordinate-based integration and abstract differential geometry. The development relies on three primary methodological pillars:

True Pullback via Fréchet Derivative: The core construction defines the pullback of a differential form $\sigma^*\omega$ using the Fréchet derivative ($fderiv$) of a globally $C^\infty$ map $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ . Unlike simple coefficient pre-composition, this definition applies the form at the image point $\sigma(x)$ to vectors pushed forward by $D\sigma(x)$ , adhering to standard differential-geometric definitions.
Reduction to Box Stokes: The proof strategy reduces the singular case to the axis-aligned box case. By leveraging mathlib4's extDeriv_pullback theorem, the authors establish the naturality identity $d(\sigma^*\omega) = \sigma^*(d\omega)$ . This allows the application of the existing box Stokes theorem (derived from mathlib4's divergence theorem) to the pulled-back form $\sigma^*\omega$ over the parameter domain $[0,1]^{n+1}$ .
Face-Matching and Chain-Level Algebra: A critical technical component is the "face-matching identity," which proves that the integral of the pulled-back form over a box boundary face corresponds exactly to the integral of the form over the corresponding singular face. Furthermore, the authors formalize the chain complex identity $\partial(\partial\sigma) = 0$ for singular chains. This is achieved not by defining a boundary homomorphism on undecorated boxes, but by constructing a sign-reversing, fixed-point-free involution on the double-boundary index set, proving that paired terms cancel algebraically.

Key Contributions
The paper delivers a comprehensive formalization comprising 44 Lean modules (approx. 4,000 lines) with 205 named declarations. The specific contributions include:

Singular Stokes Theorem: A theorem stating that for any globally $C^\infty$ map $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ and any $C^\infty$ $n$ -form $\omega$ , the integral of $\sigma^*(d\omega)$ over the unit cube equals the alternating sum of integrals of $\sigma^*\omega$ over the $2(n+1)$ faces.
Bridge Theorem: A formal proof validating that the authors' coordinate-based exterior derivative (extDerivCoord) is consistent with mathlib4's abstract extDeriv when evaluated on standard basis vectors. This ensures the coordinate implementation is mathematically sound relative to the library's abstract API.
Chain-Level Extensions: The extension of Stokes' theorem to formal $\mathbb{Z}$ -linear combinations of singular cubes (singular chains) via linearity.
$\partial^2 = 0$ Proof: A formal proof of the chain complex identity $\partial(\partial\sigma) = 0$ for singular chains, utilizing a combinatorial involution on the index set of double faces.
Dimensional Specializations: Direct instantiations of the main theorem recovering the Fundamental Theorem of Calculus (FTC), Green's Theorem, the Divergence Theorem, and 3D Gauss's Theorem, as well as integration by parts and the Leibniz rule.
Axiom Audit: Verification that the entire development depends only on the three standard Lean 4 axioms (propext, Classical.choice, Quot.sound), confirmed via 79 systematic #print axioms checks.

Results and Scope
The formalization successfully proves Stokes' theorem for:

Smooth Singular Cubes: Maps $\sigma$ that are globally smooth on $\mathbb{R}^{n+1}$ , integrated over the parameter cube $[0,1]^{n+1}$ .
Axis-Aligned Boxes: Coordinate $n$ -forms on boxes $[a,b] \subset \mathbb{R}^{n+1}$ .

The paper explicitly notes the following limitations and scope boundaries:

No Manifold Theory: The integration domain is strictly the parameter cube or a box. The work does not formalize integration over general smooth manifolds, nor does it use partitions of unity, charts, or atlases.
Global Smoothness: The singular maps are required to be $C^\infty$ on all of $\mathbb{R}^{n+1}$ , a stronger condition than smoothness on the closed cube alone. This choice was made to simplify the formalization by avoiding boundary regularity arguments and ensuring the Fréchet derivative is well-defined everywhere.
No Image-Domain Semantics: The theorem treats the integral as an operation over the parameter domain. It does not prove that the image of $\sigma$ constitutes a submanifold or an oriented geometric chain in the target space.

Significance and Claims
The authors claim this work provides the first complete Lean 4 formalization of Stokes' theorem for smooth singular cubes with a "true" differential-form pullback. Its significance lies in:

Bridging Concrete and Abstract: The "bridge theorem" pattern validates a concrete coordinate implementation against mathlib4's abstract exterior derivative, offering a reusable methodology for future formalizations.
Infrastructure Reuse: The development relies heavily on existing mathlib4 infrastructure (divergence theorem, extDeriv_pullback), demonstrating how high-level library components can be composed to prove complex geometric theorems without reinventing foundational analysis.
Complementarity: The work is complementary to Harrison's HOL Light formalization. While Harrison covers convex/polyhedral domains with gauge integration, this work covers smooth singular parametrizations using Bochner integration and mathlib4's differential geometry API.
Foundational Readiness: By proving $\partial^2=0$ and establishing the chain-level Stokes theorem, the authors provide a necessary local building block for a future full formalization of Stokes' theorem on smooth manifolds with boundary, once mathlib4's manifold integration and orientation APIs mature.

The paper concludes that while it does not solve the problem of integration on general manifolds, it establishes the critical "cubical-chain" layer with true pullbacks, serving as a verified foundation for future extensions.