Formalizing Verdier Duality

Final project for CSE 290Q: Topics in Proof Assistants.

Modern mathematics is built on the foundation of formal systems. Mathematical research can be seen as a distributed system based on reputation and trust, where verifications are conducted by hand, sometimes requiring significant effort. As mathematics gets more and more complicated, this approach faces several challenges that undermines the potential of future development of the subject.

In recent years computer-assisted proof verification has emerged as an alternative framework for writing and verifying mathematical proofs, offering novel perspective on how math research could be done in a modernized way.

This project aims to explore the possibility of formalizing mainstream mathematics using Lean proof assistant and mathlib by attempting to provide formalization for the Verdier Duality Theorem from the field of algebraic topology and algebraic geometry.

Motivation and Background

Formalization of mathematics was first proposed by G. Frege (1879), then quickly popularized by D. Hilbert’s program (1920s), and generalized to all fields of math as a shared foundation by the Séminaire Bourbaki (1939). For decades, the giant monolithic formal structure of mathematical work “relies on a complex system of mutual trust based on reputations [1]”, with proofs checked manually by other math researchers.

However, as the complexity of mathematics started to explode in the 1970s, despite the extraordinary hard work put into peer review, there are hints that this manual approach may not be sustainable in the foreseeable future.

Here I want to give two examples of this problem. The first one is a famous story of algebraic topologist Voevodesky. He was involved in the development of the groundbreaking theory of motivic cohomology in late 1980s and early 1990s, but only to find that the early papers of the subject were plagued with subtle errors that are buried deep within some technical lemmas — and because of the collaborative nature of mathematical research, these errors propagated across different authors, ruining their work, and often could not be salvaged. To make things worse, because such collaboration is based on reputation, “a technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail”, as said by Voevodesky.

Another aspect of this problem is that if there is a controversial proof for a big open problem that is so complicated that it is hard or nearly impossible to be checked by hand, it may take a very long time for the academia to reach an agreement on its validity. An example of this is the proof for Four Color Theorem. This is a conjecture raised in 1852, with a simple claim at first glance, regarding a coloring property of regions on a plane. However, it turned out to be very difficult, and all its proof attempts in the following 100 years ended up being invalid.

In 1976, Appel and Haken [2] provided a proof by an semi-brute-force approach aided by computer programs. However, this proof is highly controversial: its staggering complexity voided any hope for verifying the proof by hand, and the academia had reasonable worries about the correctness of the program used in the proof. The controversies remailed unresolved for nearly 30 years, until Gonthier and Werner [3] used a full-fledged proof assistant Coq to finally provide a formalization for it.

Mathematics as a Software

Most computer proof formalization tools depend on the Curry-Howard isomorphism, which can be briefly summarized in the following table:

Generally speaking, what these proof assistants do is to provide a way to faithfully translate a math proposition and its proof into the a typed program, and then automatically check if the program is well-formed. If this is true, (and suppose we believe that the prover behaves as expected), we are confident that the proof is logically correct.

On this ground, there are actually striking connections between formal math work and software engineering. If formalization of math are widely accepted and becomes a standard, we can adopt those already very mature methodologies of software engineering to modernize how we work with and collaborate on math.

The math community will benefit from well-defined, structured definitions and axioms in the form of interfaces, avoiding the problem of confusing variant of notations that troubled a lot of people outside of the expertise of that specific field, auto-generated, searchable math reference books similar to those produced by language-aware documentation generators like JavaDocs and rust-doc, solid “code” (proof) reuse, and mature collaboration tools like source control, static site generators, and more.

Formalizing math with Lean

The Lean proof assistant is a complicated stack of software aiming to not only perform proof verification, but also provide a framework and a toolbox of automation tools to ease the explicitness problem introduced by rigid formalization and provide a user- (i.e. mathematician) friendly way of writing proofs. The latter is very important, since building a proof verification system is relatively simple, but the hard part is to replicate the majestic tower of math construct in that language, and form an organic community of math researchers who use it for creation of new mathematics.

Lean can be roughly described as the following layers, one built upon one another:

1. A complete Implementation of a pure functional programming language (also called lean), which is required by any proof assistants based on Curry-Howard isomorphism;
2. a variant of dependent type theory, with the additional structure of construction of calculus to provide inductive construction of types;
3. a special family of types Prop, giving a model of propositions and proofs, where types of type Prop represent propositions, and terms of these propositions represent a proof of the corresponding proposition;
4. a meta programming system called tactics, using hygienic macros resembling that of Scheme, for proof automation such as generating proofs for mechanical simplification, and some basic capability of searching for theorems in the codebase to apply.

All these layers are written in the lean language itself, providing excellent self-explanatory property and extensibility. To mend the efficiency problem introduced by this approach, there is a fifth component outside of these layers, which is a C transpiler that could be invoked on manually labeled code to compile hot spots to C and then to binaries and load them back to Lean as plugins, providing an ad-hoc just-in-time feature [4].

Under this framework, verifying a given proof of a proposition translates to performing type-checks (in the sense of programming languages) of the term corresponding to the proof (the proof term) against the desired type. The proof term itself is constructed inductively by constructing terms of other inductive types using terms available, destructing existing terms to get other terms, forming functions using lambdas, or applying functions to get new terms. The proof-checker tries to recursively expand the proof term given into a large loop-free directed graph of terms, where the terms on the source nodes are supposed to be atomic terms produced by axioms (axioms are just a Prop type with guaranteed existence of a proof term), mimicking the unfolding and reductions performed when checking math proofs.

However, in reality, almost nobody will do math by going all the way back to the axioms on every math object. Instead, people use lemmas to divide-and-conquer larger proofs, decoupling the verification of a longer proof into smaller proofs of several independent lemmas, and furthermore, “package” and “export” important ones as theorems to share their results to others.

Similarly, in Lean, instead of traversing the whole “reasoning tree” we just mentioned every time, to make proof-checking computationally feasible as an interactive experience, Lean provide similar concepts of lemmas and theorems in the forms of named symbols, whose types (and equivalently, validity of proofs) can be checked in parallel. One big benefit of this approach is that the proof of a big result can be done non-linearly by assuming the correctness of certain lemmas while working on others, and finally filling all the gaps.

Verdier Duality

The target of this project is to formalize Verdier duality. Verdier duality theorem is a generalization of the well-known Poincaré duality theorem. The latter gives insights into some patterns of (co)homological duality for a class of very well-behaved spaces — closed and oriented manifolds, and Verdier duality generalize this result to a vastly larger class of geometric objects, by the usage of sheave theory as a general language for different kinds of geometry. On the other hand, Verdier duality is itself an important concrete example of Grothendieck’s six-functor formalism, making it a connective result between algebraic topology and algebraic geometry. The theorem is given in the form of existence of an adjoint on the level of derived categories:

Here, denotes the derived category of bounded chains of sheaves of modules over a ring on given topological space, denotes the functor of direct image with proper support, is the internal sheaf hom complex, and denotes the right derived functor of a given functor.

By attempting to formalize this theorem, we could testify the matureness of mathlib—whether or not it is prepared for working with this field of math that is known for heavy machinery, and gain some insights on how far it is for Lean to become a solid tool for math research, and what infrastructure is still missing in mathlib.

Implementation

I provide some details of implementation of this project, with the aim of giving a sense of the actual experience of working on a Lean project.

For the rest of the section, we fix two topological spaces and that are locally compact Hausdorff, and a Noetherian commutative ring :

variable  (X : TopCat.{u}) [LocallyCompactSpace.{u} X] [T2Space.{u} X]
          (Y : TopCat.{u}) [LocallyCompactSpace.{u} Y] [T2Space.{u} Y]
          (R : Type w) [CommRing.{w} R] [IsNoetherianRing.{w} R]

The way that we declare the variable for the ring may seem unexpected at the first glace (why not: R : CommRing?), but this is actually paying the debt of abuse of notation that became natural to mathematicians: when we talk about the ring , we are actually mixing up the actual math structure and the carrier set . The model that Lean uses for a specific ring, on the other hand, is to let the carrier set to be any type, and augment ring operations using type classes (cite: How to make ad-hoc polymorphism less ad hoc) similar to the same term in Haskell.

The TopCat.{u} notation is for explicit universe level polymorphism and will be discussed in later sections.

We denote the category of sheaves of -modules over a topological space by . After stating some of its basic properties, we can upgrade it to the category of chain complexes of sheaves, and then its corresponding derived category .

abbrev Sh (base : TopCat.{u}) : Type (max u (v + 1) w)
  := TopCat.Sheaf.{u, v, (max w (v + 1))} (ModuleCat.{v, w} R) base

instance (base : TopCat) : Preadditive (Sh R base) := ...
instance (base : TopCat) : Abelian (Sh R base) := ...
instance (base : TopCat) : HasDerivedCategory (Sh R base) := ...

abbrev C (base : TopCat.{u}) : Type (max u (v + 1) w)
  := CochainComplex (Sh.{v} R base) ℤ

instance (base : TopCat) : Abelian (C R base) := ...
instance (base : TopCat) : HasDerivedCategory (C R base) := ...

abbrev D (base : TopCat.{u}) : Type (max u (v + 1) w)
  := DerivedCategory.{v'} (C.{v} R base)

Next, we construct functions that let us construct direct image functor, and upgrade this functor to work on chain complexes, and then on derived category. We claim that they are additive.

def direct_image (f : X → Y) (p_cont : Continuous f) :
  Sh.{v, u} R X ⥤ Sh.{v, u} R Y where ...
def direct_image_proper_support (f : X → Y) (p_cont : Continuous f) :
  Sh.{v, u} R X ⥤ Sh.{v, u} R Y where ...
instance (f : X → Y) (p_cont : Continuous f) :
  Functor.Additive (direct_image_proper_support.{v, u} X Y R f p_cont) := ...

Here demonstrates another practice used by Lean that may be confusing: if we want to put restrictions on the type of argument of a function, we would declare additional instance implicit arguments:

def foo (x : BaseTypeAlpha) [RestrictionOne x] : BaseTypeBeta := ...

but there is no dual way to add additional restriction to BaseReturnType, causing troubles when trying to compose a bunch of functions with complicated input types:

def bar (x : BaseTypeBeta) [RestrictionTwo x] : BaseTypeGamma := ...

-- The following gets an type class resolution error:
abbrev foobar (x : BaseTypeAlpha) := bar (foo x)

The solution to this problem in Lean is somewhat ad-hoc:

instance (x : BaseTypeAlpha): RestrictionTwo (foo x) := ...

and it turns out that this approach may go wrong at some times: the Functor.Additive instance we registered could not be looked up by Lean afterwards, and I suppose it is a bug. I hope there could be a better way to express such return type constrain in the future.

Then we do the same bunch of definitions and property claims for sheaf homs:

def sheaf_hom (F G : Sh.{v, u, w} R X) :
  Sh.{v, u, w} R X := ...
def sheaf_hom_complex (F G : C.{v, u, w} R X) :
  C.{v, u, w} R X := ...
def derived_sheaf_hom_complex (F G : D.{v, v', u, w} R X) :
  D.{v, v', u, w} R X := ...

and define the right derived functor for given chain functor:

def derived (F : C.{v, u, w} R X ⥤ C.{v, u, w} R Y) :
  D.{v, v', u, w} R X ⥤ D.{v, v', u, w} R Y := ...

Then, finally we can state the main theorem:

variable
  (f : X → Y)(p_cont : Continuous f)
  (F : D.{v, v', u, w} R X) (G : D.{v, v', u, w} R Y)

theorem local_verdier_duality :
  ∃ g : D.{v, v', u, w} R Y ⥤ D.{v, v', u, w} R X,
  Nonempty (Iso
    (derived_sheaf_hom_complex.{v, v', u, w} Y R
      ((R!.{v, v', u, w} X Y R f p_cont).obj F) G)
    ((Rstar.{v, v', u, w} X Y R f p_cont).obj
      (derived_sheaf_hom_complex.{v, v', u, w} X R F (g.obj G))))
  := sorry

Lean blueprint

Limited by the length of the beloved quarter system, I only managed to formalize the prerequisite definitions (with a lot of proof gaps to ensure the definitions are valid) and state the theorem, but the proof of this theorem has not been started at all. And the original goal of this project, to fully formalize the proof of this theorem, turns out to be way too ambitious, as the original proof for Verdier duality runs over 50 pages.

However, one of, if not the most important goal of software engineering, is to limit the complexity and distribute the work temporally (i.e. sustainable long-term project) and spatially (i.e. across multiple collaborators). There is a tool from the Lean ecosystem that can help with the situation—Lean blueprint. This is an example of automated tools inspired by existing software engineering practices and made possible by the programmable nature of Lean.

A Lean blueprint [6] is a standard LaTeX document that gives an outline of the whole formalization project, with lemmas augmented with information that links each of them to the corresponding definition in the codebase. This document can be compiled to a PDF or a static website, and the tool will check the implementation status of each lemma and mark the progress on the document or website it generates, making it a useful project management tool. Once the blueprint is established, the project could move on more efficiently by crowd-source from the community and become a large-scale, collaborative formalization effort. Many famous Lean projects are using this approach, as listed in [6].

Reflection and Discussion

It turns out that even reaching the point of stating the Verdier duality theorem is a hard process. This is due to multiple reasons: the intrinsic complexity of the math material itself, the added difficulty of formalization, and some current caveats of the design and the ecosystem of Lean itself. In this section, I will share some thoughts that I had during the process of working on this project.

Current status of documentation

Currently Lean has several different kinds of documentations: a set of rust-book-styled tutorials covering different aspects of Lean (theorem proving, functional programming, meta-programming, and doing math), a language reference, and a documentation generator called doc-gen4 [7] to generate doc from source code.

Currently it is not very clear to find and navigate between these resources, and the completeness of documentation is definitely not enough. The source code style in Lean is highly flexible, concise but complicated, and often confusing to someone new to it. This problem is especially serious when trying to find some piece of code for some math concept in mathlib, since most math objects are highly polymorphic —if two things are similar in spirit, then mathematicians like to just use the same term for simplicity. For example, the term of “presheaf” could indicate three subtly different things:

1. Any contravariant functor, the most abstract one;
2. a contravariant functor from the category of opens to the category of modules over fixed ring , frequently seen in algebraic topology;
3. a contravariant functor where the ring is determined by another contravariant functor on the site, mostly appear in the context of algebraic geometry.

The are all roughly talking about the same thing, and in theory they can be turned into each other via some code composition, but it turns out that the glue code for that purpose is not easy to work out; to make things worse, code about the first and the third concept is scattered in different places in the codebase, with each occurrence adding some definitions, theorems or instances, making it really hard to find or construct the desired mathematical structure.

There are several things that are potentially able to help out with this situation. The first one is the approach of schematic search engine for Lean code [8]. It first use an LLM to deformalize the signature of each mathlib definition and theorem into natural language, and then use a traditional search engine to search through the natural language terms to find the corresponding formalization.

This is a clever way of utilizing the power of LLMs to help with Lean projects but avoiding their shortcomings: LLMs often do a terrible job when asked to generate very formalized content that satisfy certain constrains—they often make up something that does not exist or just end up with a bunch of nonsense—but they are very good at deformalize things and generate natural language. Such idea is made into an instance called Lean search. There is another tool called Moogle, probably based on the same idea, but its mechanism is not made public yet.

On the other hand, there is an ongoing effort, Mathlib.StacksTag, to link items in some semi-formalized mathematical wikis, like the Stacks project and Kerodon, with components in mathlib using some extensible code attributes, powered by Lean’s meta-programming capability, which I think is the ultimate solution in the long run. Building a complete formalized correspondence between mainstream math textbooks and mathlib will drastically reduce the difficulty for the larger math community to adopt Lean as a daily tool.

Problem with universes

Since we have moved to a rigid, automated system for proof verifications, we are no longer able to drive away those logic problems that are not of interest to mathematicians (for example, the infamous Russell’s paradox) by just waiving our hand.

The approach taken by Lean is fairly strict: it requires you to be explicit on the universe level of each type, either by stating the actual level number, or by using universe level polymorphisms. Lean tries ease the workload of figuring out universe levels by providing universe level inference as part of the type inference package. However, compared to the unbelievably strong capability of the rest of the inference package, this universe level inference is very conservative, as it doesn’t know if the user intends to have this much generality, or, in most cases, neither have been aware of such generality nor want it to be in their definitions and proofs. And when the elaborator is not sure, it adds yet another layer of universe polymorphism.

As a result, the universe level goes up uncontrollably fast, and sometimes results in universe level overflow that leads to failure of verification. This frustration appears frequently when dealing with categories and higher hierarchy of layered definitions, which are very common in modern math.

Summary

This report begins by investigating the rationale of formalizing mathematics using proof assistants in general, and outlines how Lean 4 proof assistant realizes this goal, with the hope of providing a high-level overview to readers unfamiliar with formal methods. The second part of this report documents my attempt to formalize the Verdier Duality theorem, a nontrivial result in modern mathematics. This is followed by a reflection on the current challenges of popularizing Lean in the math community.

References