arxiv: 2605.01028 · v1 · submitted 2026-05-01 · 💻 cs.LO · math.DG

Recognition: unknown

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

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

Authors on Pith no claims yet

Pith reviewed 2026-05-09 17:50 UTC · model grok-4.3

classification 💻 cs.LO math.DG

keywords Stokes theoremformalizationLean 4singular cubesFréchet derivativedifferential formsmathlib4exterior derivative

0 comments

The pith

Stokes theorem for smooth singular cubes in any dimension is formally proved in Lean 4 using Fréchet derivative pullbacks.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The authors deliver a complete formalization in Lean 4 of Stokes theorem that covers smooth singular cubes of arbitrary dimension. They accomplish this by implementing the pullback of differential forms through the Fréchet derivative to ensure it is the genuine operation rather than a simplified version. The work further develops supporting results such as the vanishing of d squared on cubical chains and special cases like box Stokes theorem. This matters to a reader interested in reliable computational mathematics because it creates a verified base that aligns with classical analysis and can support additional proofs.

Core claim

The paper establishes a sorry-free formalization of Stokes' theorem for smooth singular cubes in arbitrary dimension within Lean 4 and mathlib4. It relies on the true pullback of differential forms defined using the Fréchet derivative. Additional results include extensions to chain-level applications with Z-linearity, proof of d squared equals zero for singular cubical chains, and connections to other library components.

What carries the argument

True differential-form pullback defined via the Fréchet derivative for smooth maps on singular cubes.

Load-bearing premise

The Fréchet derivative and smooth map definitions in the Lean 4 libraries correspond exactly to their classical counterparts in analysis.

What would settle it

Finding a specific smooth singular cube and differential form where the formalized Stokes theorem gives a result different from the classically computed integral would show the formalization does not capture the intended theorem.

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

A careful sorry-free Lean 4 formalization of Stokes' theorem for singular cubes that adds a true Fréchet pullback and chain-level d²=0 to mathlib4.

read the letter

This paper gives a machine-checked Lean 4 development of Stokes' theorem for smooth singular cubes in any dimension. The core is a true differential-form pullback defined via the Fréchet derivative rather than a simplified version, plus an extension to Z-linear singular cubical chains that proves d²=0 at the chain level. They also include box Stokes for axis-aligned cubes, dimensional reductions, and a direct comparison with Harrison's earlier HOL Light work. All of it is sorry-free and built against mathlib4 definitions, which is the main new piece. The formalization supplies reusable pieces like the pullback bridge to extDeriv that others can use without redoing the analytic groundwork. The soundness rests on the fact that the entire development is verified inside the system, so internal consistency is not in doubt. The only real question is how closely the library's smooth maps and Fréchet derivative match the classical objects, but the authors flag this as an explicit bridge rather than hiding it. That is standard for these projects and does not look like a load-bearing gap here. The work is aimed at people already working in Lean formalizations of differential geometry or analysis. A reader who needs a verified Stokes theorem to build higher results on, or who wants to see how Fréchet pullback is handled in practice, will find concrete code and proofs to inspect. It is narrow but technically solid, so it deserves a serious referee who can check the Lean scripts and the comparison section. I would send it out for review rather than desk-reject; the contribution is narrow enough that heavy revision is likely, but the verified artifact itself is worth external scrutiny.

Referee Report

0 major / 1 minor

Summary. The manuscript presents a sorry-free Lean 4/mathlib4 formalization of Stokes' theorem for smooth singular cubes in arbitrary dimension. It defines pullback of differential forms via the Fréchet derivative, bridges to mathlib4's abstract extDeriv, extends Stokes to Z-linear singular cubical chains, proves d²=0 at the chain level, provides box Stokes for axis-aligned cubes and dimensional specializations, and includes a structured comparison with Harrison's HOL Light formalization.

Significance. If the formal notions align with their classical counterparts, the result supplies a verified, reusable component for differential geometry and algebraic topology inside the Lean ecosystem. The machine-checked, sorry-free status, direct use of library primitives, and chain-level extensions (including d²=0) constitute concrete strengths that lower the barrier for subsequent formal work. The explicit comparison with prior HOL Light development further aids assessment of scope and approach.

minor comments (1)

The abstract and introduction repeatedly use the phrase 'true pullback' without an immediate pointer to the precise definition or lemma that implements it; a parenthetical reference to the relevant section or equation would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the manuscript, the recognition of its sorry-free status, direct use of mathlib4 primitives, chain-level extensions, and the structured comparison to prior HOL Light work, and for the recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity: machine-checked formalization against external library definitions

full rationale

The paper presents a sorry-free Lean 4 formalization of Stokes' theorem for smooth singular cubes, relying on mathlib4's definitions of Fréchet derivative, smooth maps, and singular cubes. The central claim is a verified proof inside the theorem prover, not a derivation that reduces to fitted parameters, self-defined quantities, or load-bearing self-citations. The only correspondence to classical mathematics is treated explicitly as a bridge rather than an unexamined assumption. No steps match the enumerated circularity patterns; the development is self-contained against the external mathlib4 benchmark and Harrison's independent HOL Light work.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The formalization rests on standard mathematical definitions of Fréchet derivatives, smooth maps, and singular cubes already present in mathlib4; no new free parameters, ad-hoc axioms, or invented entities are introduced.

axioms (2)

standard math The Fréchet derivative correctly implements the classical notion of differentiability for maps between Banach spaces.
Invoked when defining true pullback of differential forms.
domain assumption Smooth singular cubes form a chain complex whose boundary operator satisfies the usual algebraic properties.
Required for the chain-level extension of Stokes' theorem and d²=0.

pith-pipeline@v0.9.0 · 5400 in / 1424 out tokens · 26170 ms · 2026-05-09T17:50:48.675864+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

17 extracted references · 12 canonical work pages

[1]

Abdulaziz and L

M. Abdulaziz and L. C. Paulson,An Isabelle/HOL formalisation of Green’s theorem, Journal of Automated Reasoning, 63(3):763–786, 2019.doi: 10.1007/s10817-018-9495-z

work page doi:10.1007/s10817-018-9495-z 2019
[2]

A. Best, C. Birkbeck, R. Brasca, E. Rodriguez Boidi, R. Van de Velde, A. Yang,A com- plete formalization of Fermat’s Last Theorem for regular primes in Lean, Annals of Formalized Mathematics, 1:103–132, 2025.doi: 10.46298/afm.14586. 23

work page doi:10.46298/afm.14586 2025
[3]

Bott and L.W

R. Bott and L. W. Tu,Differential Forms in Algebraic Topology, Graduate Texts in Mathe- matics, vol. 82, Springer, 1982.doi: 10.1007/978-1-4757-3951-0

work page doi:10.1007/978-1-4757-3951-0 1982
[4]

In: Au- tomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings

L. de Moura and S. Ullrich,The Lean 4 theorem prover and programming language, CADE-28, 2021.doi: 10.1007/978-3-030-79876-5_37

work page doi:10.1007/978-3-030-79876-5_37 2021
[5]

Gouëzel,Smooth manifolds in Lean, contributed tomathlib4; seeMathlib.Geometry.Manifold.SmoothManifoldWithCorners,https:// leanprover-community.github.io/mathlib4_docs/

S. Gouëzel,Smooth manifolds in Lean, contributed tomathlib4; seeMathlib.Geometry.Manifold.SmoothManifoldWithCorners,https:// leanprover-community.github.io/mathlib4_docs/
[6]

Harrison,A HOL theory of Euclidean space, TPHOLs 2005, Springer LNCS 3603, pp

J. Harrison,A HOL theory of Euclidean space, TPHOLs 2005, Springer LNCS 3603, pp. 114– 129, 2005.doi: 10.1007/11541868_8

work page doi:10.1007/11541868_8 2005
[7]

Harrison,The HOL Light theory of Euclidean space, Journal of Automated Reasoning, 50(2):173–190, 2013.doi: 10.1007/s10817-012-9250-9

J. Harrison,The HOL Light theory of Euclidean space, Journal of Automated Reasoning, 50(2):173–190, 2013.doi: 10.1007/s10817-012-9250-9

work page doi:10.1007/s10817-012-9250-9 2013
[8]

2009.A Statistical Learning Perspective of Genetic Programming

J. Hölzl, F. Immler, and B. Huffman,Type classes and filters for mathematical analysis in Isabelle/HOL, ITP 2013, Springer LNCS 7998, pp. 279–294, 2013.doi: 10.1007/978-3-642- 39634-2_21

work page doi:10.1007/978-3-642- 2013
[9]

Y. Kudryashov,Divergence theorem for Henstock–Kurzweil integrals in mathlib, con- tributed tomathlib4; cited viaintegral_divergence_of_hasFDerivAt_off_countable’in Mathlib.MeasureTheory.Integral.DivergenceTheorem,https://leanprover-community. github.io/mathlib4_docs/
[10]

Y. Kudryashov,Exterior derivative and differential forms in mathlib, contributed tomathlib4; seeMathlib.Analysis.Calculus.DifferentialForm.Basic,https: //leanprover-community.github.io/mathlib4_docs/
[11]

J. M. Lee,Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics, vol. 218, Springer, 2012.doi: 10.1007/978-1-4419-9982-5

work page doi:10.1007/978-1-4419-9982-5 2012
[12]

The mathlib Community,Mathlib4: The Lean 4 Mathematical Library,https://github.com/ leanprover-community/mathlib4, 2024–2026

2024
[13]

In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

The mathlib Community,The Lean mathematical library, CPP 2020, pp. 367–381, ACM, 2020. doi: 10.1145/3372885.3373824

work page doi:10.1145/3372885.3373824 2020
[14]

Spivak,Calculus on Manifolds, W

M. Spivak,Calculus on Manifolds, W. A. Benjamin, New York, 1965

1965
[15]

van Doorn and H

F. van Doorn and H. Macbeth,Integrals within integrals: A formalization of the Gagliardo–Nirenberg–Sobolev inequality, ITP 2024, LIPIcs vol. 309, 2024.doi: 10.4230/LIPIcs.ITP.2024.37

work page doi:10.4230/lipics.itp.2024.37 2024
[16]

37–55 (05 2021)

F. van Doorn, G. Ebner, and S. Lewis,Maintaining a library of formal mathematics, Intelligent Computer Mathematics (CICM 2020), Springer LNAI 12236, 2020.doi: 10.1007/978-3-030- 53518-6_16

work page doi:10.1007/978-3-030- 2020
[17]

Whitney,Analytic extensions of differentiable functions defined in closed sets, Transactions of the AMS, 36(1):63–89, 1934.doi: 10.2307/1989708

H. Whitney,Analytic extensions of differentiable functions defined in closed sets, Transactions of the AMS, 36(1):63–89, 1934.doi: 10.2307/1989708. 24

work page doi:10.2307/1989708 1934