About a month ago, the Cauchy integral theorem for some simple domains landed in mathlib. PR number 10000 was specially allocated for this occasion in advance. In this post I will recollect the events that led to this formalization.

Unlike all other formalizations of the Cauchy integral formula, this one is based on a very general version of the divergence theorem. I discuss the technical decisions behind this formalization in a paper I have recently submitted to the ITP conference.

The simplest version of the divergence theorem says that for a continuously differentiable vector field $v$ on a rectangular box $I$ in $ℝ^n$, the integral of the divergence $\operatorname{div} v$ over $I$ is equal to the flux of $v$ through the boundary of $I$, where the flux of $v$ through $i$-th front (resp., back) face of $I$ is defined as plus (resp., minus) the integral of $v_i$ over this face.

The Cauchy integral theorem (a.k.a. the Cauchy-Goursat theorem) states that the integral $\oint_\gamma f(z)\,dz$ is equal to zero provided that $f$ is complex differentiable in the domain bounded by $\gamma$. For simplicity, let us consider only rectangular domains.

If $f:ℂ → ℂ$ is continuously differentiable on this rectangle, then the Cauchy-Goursat theorem for $f$ on this rectangle follows from the divergence theorem applied to the vector field $v_{f}(x, y)=(\operatorname{Re} f(x+iy), -\operatorname{Im} f(x+iy))$.

Many students (including me) were taught that this argument can't be patched to work for any differentiable function, and one has to use a trick specific to complex analysis (e.g., an explicit infinite descent on triangles). In October 2020, we had a chat on Zulip about formalization of complex analysis, where Patrick Massot shared a link to a paper by Felipe Acker where Felipe proves the divergence theorem for a differentiable vector field with continuous divergence. The vector field $v_f$ introduced above has divergence zero, hence this version of the divergence theorem implies the Cauchy-Goursat theorem.

I started formalizing a simplified version of Acker's proof right away, and had a draft version by November 2020. Later I dropped this version, but some traces of this attempt can be found in this abandoned pull request.

Once I had the first draft, I realized that the proof reminded me of the proof of the Fundamental Theorem of Calculus for the Henstock-Kurzweil integral. I had heard about this integral when I was a student at the Moscow State University, and some of my classmates complained that their professor Lukashenko¹ made them study the useless Henstock integral as a part of a standard 1st year analysis course.

So, I opened some old lecture notes written by my classmates, refreshed my knowledge of the Henstock integral, and realized that actually I prove that the divergence is integrable in the sense of one of possible generalizations of this integral to $ℝ^n$. Thus I decided to formalize the Henstock integral in Lean and split the proof into two parts: the divergence theorem for a Henstock-like integral that required no regularity from the divergence, and a proof of the fact that any Bochner integrable function is Henstock integrable.

During most of 2021 I worked on other projects but in the fall I came back to the divergence theorem and formalized it. The university library was closed because of the pandemic and I failed to find a good source on the multivariable Henstock integral online, so I had to generalize theorems myself.

The most difficult part was to formalize the notion of a Henstock/McShane/Riemann integral (it took more than 4000 lines) and figure out what parts of the one-dimensional proofs I had at hand work in the multivariable settings.

In October 2021, I formalized the divergence theorem for a Henstock-style integral and by the first days of January I had the Cauchy-Goursat theorem. This opened a door to formalization of other topics in complex analysis, and I have already formalized the Riemann removable singularity theorem (merged) and the maximum modulus principle (pending API update and review). Moreover, Jireh Loreaux already used my new additions to the library to prove Gelfand's formula for the spectral radius, pending review.

In January 2022, I decided to write an ITP paper about this project. While searching for references for the paper, I found a survey by Benedetto Bongiorno. I still can't understand why I didn't find this survey half a year earlier (I found it by googling for something like "Henstock integral divergence theorem"). I read the survey and found out that the version of the Henstock-Kurzweil integral I used in the project was introduced by Mawhin about 5 years before I was born, and there are several more advanced definitions that allow us to prove the divergence theorem with even weaker assumptions (e.g., with one of the integrals one can replace the differentiability assumption by continuity on a countable set of hyperplanes).

For a few days, I was unsure whether I should proceed with my paper or implement one of these integrals first. Then I decided to write about the completed project and write about other integrals in the "Future plans" section.