Skip to main content

Hoskinson Center announced

On September 22, 2021, Carnegie Mellon University announced that a $20 million gift from blockchain entrepreneur Charles C. Hoskinson will be used to establish the Hoskinson Center for Formal Mathematics, housed in the Department of Philosophy. You can read the university press release and watch Hoskinson's YouTube announcement. You can also watch Hoskinson's presentation and my presentation at an inauguration ceremony that was held at Carnegie Mellon the day before. The slides I used for the presentation are here.

The center's mission is to support the work being done by the Lean community, to promote the use of Lean and its libraries, and to seek out ways of using the technology to make mathematics accessible and enjoyable to as wide an audience as possible.

The initial endowment will be used to support postdoctoral researchers and graduate students, as well as occasional meetings and visitors. In the near future, the center will focus on supporting the port of mathlib to Lean 4, developing automation and the user interface, and, perhaps most importantly, preparing textbooks and educational materials based on Lean.

This month in mathlib (Sep 2021)

This post summarizes some of the activity that happened in mathlib in September.

Highlighted PRs

  • Number fields. The Dedekind saga continues with PR #8847, PR #8701 (define number fields, rings of integers), PR #8949, PR #8964, and PR #9063, culminating in PR #9059 which shows that, in the presence of an admissible absolute value, the class group of an integral closure is finite.
  • Probability theory. Foundations of probability theory are (finally!) coming to mathlib. With PR #8939 and PR #8920 (conditional expectation of an indicator) the way was open for PR #9114 which defines the conditional expectation of a function.
  • Algebraic closures. Over two years ago, PR #1297 was opened, showing that algebraic closures are unique (up to non-unique isomorphism). Due to various issues, the material was not yet in shape for inclusion in mathlib. Over summer, the material got a facelift, leading to PR #9110, PR #9231, and PR #9376. There probably are no other commits that had to wait so long before being merged into mathlib.
  • Riesz theorem on compact unit ball and finite dimension. Mathlib now knows the main difference between the topology of real normed spaces in finite and infinite dimensions: the closed unit ball in such a space is compact if and only if the space is finite dimensional. The implication from finite dimension to compactness was proved in PR #1687 and PR #9147 proves the converse.
  • Measure theory. PR #9325 shows that any additive Haar measure on a finite-dimensional real vector space is rescaled by a linear map through its determinant, and computes the measure of balls and spheres. PR #9065 adds Radon-Nikodym and Lebesgue decomposition for signed measures, see this blogpost for more details.
  • Henselian local rings. PR #8986 sets up the theory of Henselian rings. A ring $R$ is Henselian at an ideal $I$ if the following conditions hold:
    • $I$ is contained in the Jacobson radical of $R$
    • for every polynomial $f$ over $R$, with a simple root $a₀$ over the quotient ring $R/I$, there exists a lift $a ∈ R$ of $a₀$ that is a root of $f$.
  • Semilinear maps. Several people undertook a massive refactor to generalize linear maps to semilinear maps. This opens the door for the use of semilinear maps in functional analysis, but also Frobenius semilinear maps in characteristic $p > 0$. PR #8857 introduces notation for linear_map.comp and linear_equiv.trans which makes it easy to work with identity-semilinear maps (aka, linear maps) without getting distracted by the redundant semilinearity conditions. With this notation in place, PR #9272 performs the actual redefinition of linear_map and linear_equiv to be semilinear.
  • Convexity refactor. Another ongoing refactor aims to massively generalize and restructure material on convex sets/functions. One of the gems in a long stream of PRs shows that it is now trivial to deduce concave results from their convex counterparts: PR #9356 generalizes lemmas about convexity/concavity of functions, and proves concave Jensen.

Other mathematical contributions

The following PRs are ordered by the date that they were merged into mathlib.

  • PR #8894: add topological localization
  • PR #8962: Prove (co)reflectivity for Kan extensions
  • PR #8801: class formula, Burnside's lemma
  • PR #8947: Define homotopy between functions
  • PR #8946: rigid (autonomous) monoidal categories
  • PR #8579: one-point compactification of a topological space (the Stone-Cech compactification had been around for ages, and now its little brother joined the gang)
  • PR #9165: upgrade to Lean 3.33.0c
  • PR #9288: Sylow's theorems for infinite groups

The Radon-Nikodym theorem in Lean

I have for the past two months been working on formalising the Radon-Nikodym theorem in Lean, and with PR #9065 merged into mathlib, this journey seems to have finally come to an end.

The Radon-Nikodym theorem provides a necessary and sufficient condition for comparing two measures, and allows us (under certain conditions) to express one measure in terms of another. The Radon-Nikodym theorem is an important result in measure theory and has a wide range of applications in different fields of mathematics. Most notably, it can be applied in probability theory in the definition of the conditional expectation and in mathematical finance through the Girsanov theorem1.

Given two measures $\mu$ and $\nu$ on $\alpha$, we say that $\mu$ is absolutely continuous with respect to $\nu$ (and write $\mu \ll \nu$) if for all subsets $S$ of $\alpha$, $\nu(S) = 0$ implies $\mu(S) = 0$. Absolute continuity is an important notion for measures and we would like to establish a condition for when it is true.

Given a measure $\mu$ on $\alpha$ and a measurable function $f : \alpha \to \overline{\mathbb{R}}_{\ge 0}$, the set function $$S \mapsto \int_S f \text{ d} \mu$$ is also a measure on $\alpha$ and we denote this measure by $f\mu$. It is easy, and intuitive to see that $f\mu \ll \mu$, however, it is not clear whether the reverse is true. The Radon-Nikodym theorem proves the reverse implication for certain measures. In particular, the classical Radon-Nikodym theorem states that two $\sigma$-finite measures $\mu, \nu$ satisfy $\mu \ll \nu$ if and only if there exists a measurable function $f$ such that $\mu = f\nu$. This function is known as the Radon-Nikodym derivative (denoted by $\frac{\text{d}\mu}{\text{d}\nu}$) and is essentially unique whenever it exists.

In Lean, this is shown by absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq and can be found in measure_theory/decomposition/radon_nikodym. While Radon-Nikodym is the main motivation, the proof of the theorem itself is rather simple once we have the prerequisites, and thus, the project spanned over multiple files, most of which can be found in measure_theory/decomposition.

Of all the prerequisites, the most important are the Jordan decomposition theorem and the Lebesgue decomposition theorem. The Jordan decomposition theorem uniquely classifies signed measures and allows us to express every signed measure as a difference between two (mutually singular) positive measures. While the theorem itself follows from the signed Hahn decomposition, defining the structure of Jordan decompositions in Lean was tricky. While initially, the decomposition was defined as a proposition, thanks to the suggestions from the maintainers, it was decided to define the decomposition as a structure.

structure jordan_decomposition (α : Type*) [measurable_space α] :=
(pos_part neg_part : measure α)
[pos_part_finite : is_finite_measure pos_part]
[neg_part_finite : is_finite_measure neg_part]
(mutually_singular : pos_part ⊥ₘ neg_part)

This was important, as later on, it was discovered that we were able to relax some conditions on the uniqueness property of the Lebesgue decomposition by introducing scalar multiplication on Jordan decompositions2. Furthermore, as we would often like to transport between signed measures and Jordan decompositions, it is easier to work with types rather than propositions since this required a construction of an equivalence between the two types.

A similar situation was reached with the Lebesgue decomposition. The Lebesgue decomposition states that given two $\sigma$-finite measures $\mu$ and $\nu$, there exists an essentially unique measurable function $f : \alpha \to \overline{\mathbb{R}}_{\ge 0}$  and a unique finite measure $\xi$ such that $\xi$ is mutually singular with respect to $\nu$ (denoted $\xi \perp \nu$) and $\mu = \xi + f\nu$. As with the Jordan decomposition theorem, it was not clear how to represent this statement. In particular, it is important for us to be able to extract the aforementioned $f$ from the decomposition as this is the Radon-Nikodym derivative. After some experiments, I decided to represent this condition using a class.

class measure.have_lebesgue_decomposition (μ ν : measure α) : Prop :=
(lebesgue_decomposition :
   (p : measure α × (α  0)), measurable p.2  p.1 ⊥ₘ ν  μ = p.1 + ν.with_density p.2)

Since in order to prove the Lebesgue decomposition for $\sigma$-finite measures, we will first need to show it for finite measures, this definition allows us to reuse the same statement for both cases, avoiding duplicate code. Furthermore, as we would like to extract the measure and measurable function from the decomposition, we may define functions that choose the decomposition if it exists, and are zero otherwise.

def measure.singular_part (μ ν : measure α) : measure α :=
if h : have_lebesgue_decomposition μ ν then (classical.some h.lebesgue_decomposition).1 else 0

def measure.radon_nikodym_deriv (μ ν : measure α) : α  0 :=
if h : have_lebesgue_decomposition μ ν then (classical.some h.lebesgue_decomposition).2 else 0

With the Lebesgue decomposition for $\sigma$-finite measures formalized, the Radon-Nikodym theorem follows easily by considering that the singular part of the Lebesgue decomposition is zero in the case that $\mu \ll \nu$.

theorem absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq
  {μ ν : measure α} [have_lebesgue_decomposition μ ν] :
  μ  ν  ν.with_density (radon_nikodym_deriv μ ν) = μ

Furthermore, the generalisation of the Radon-Nikodym theorem to signed measures follows, simply by utilising the Jordan decomposition and realising the Radon-Nikodym derivative of the signed measure is the difference of the Radon-Nikodym derivatives of the parts of the Jordan decomposition. However, using this definition of the Radon-Nikodym derivative for the signed measures poses a problem, in which proving any properties about them requires an absolutely continuous condition. Thus, it was decided to generalise the Lebesgue decomposition theorem for signed measures from which we obtain the general Radon-Nikodym theorem.

Similar to the Lebesgue decomposition for the positive measures, the Lebesgue decomposition between a signed measure and a positive measure states that, given a signed measure $s$ and a $\sigma$-finite measure $\mu$, there exists an essentially unique measurable function $f : \alpha \to \mathbb{R}$ and a unique signed measure $t$, such that $t \perp \mu$ and $s = t + f\mu$. While this version of the Lebesgue decomposition was also represented as a class, the statement itself was modified to be an equivalent, yet easier to work with statement. Namely, a signed measure $s$ has Lebesgue decomposition with respect to a measure $\mu$ if both parts of the Jordan decomposition of $s$ have Lebesgue decomposition to $\mu$.

class signed_measure.have_lebesgue_decomposition 
  (s : signed_measure α) (μ : measure α) : Prop :=
(pos_part : s.to_jordan_decomposition.pos_part.have_lebesgue_decomposition μ)
(neg_part : s.to_jordan_decomposition.neg_part.have_lebesgue_decomposition μ)

By the same rationale, the singular part and the Radon-Nikodym derivative of the decomposition are defined similarly.

def signed_measure.singular_part (s : signed_measure α) (μ : measure α) : signed_measure α :=
(s.to_jordan_decomposition.pos_part.singular_part μ).to_signed_measure -
(s.to_jordan_decomposition.neg_part.singular_part μ).to_signed_measure

def signed_measure.radon_nikodym_deriv (s : signed_measure α) (μ : measure α) : α   := λ x,
(s.to_jordan_decomposition.pos_part.radon_nikodym_deriv μ x).to_real -
(s.to_jordan_decomposition.neg_part.radon_nikodym_deriv μ x).to_real

Using these definitions, the Lebesgue decomposition theorem was proved easily and thus, also the Radon-Nikodym theorem for signed measures. Most importantly, however, as these definition do not require an absolutely continuous condition, it was possible to prove that the Radon-Nikodym derivative $\frac{\text{d}\mu}{\text{d}\nu}$ is essentially unique without requiring $\mu \ll \nu$.

As the Radon-Nikodym theorem is central to many concepts in probability theory, a brand new territory in mathlib is now available for us to explore,
and with PR #9065 merged into mathlib, a new journey seems about to begin.


  2. Given a signed measure s, a measure μ and a real number r, one may show (r • s).singular_part μ = r • s.singular_part μ without requiring have_lebesgue_decomposition s μ by proving that the scalar product with a real number and the equivalence between signed measures and Jordan decompositions commute. 

Alex Best’s type class generalization paper

Alex J. Best wrote a paper about type class generalization for the CICM 2021 conference on intelligent computer mathematics.

When producing large formally verified mathematical developments that make use of typeclasses as in mathlib, it is easy to introduce overly strong assumptions for theorems and definitions. This paper considers the problem of recognizing from the elaborated proof terms when typeclass assumptions are stronger than necessary. It uses a Lean metaprogram that finds and informs the user about possible generalizations.

A nice example from the paper deals with the following theorem stating that given a ring homomorphism between two fields and a natural number $p$, one of the fields has characteristic p if and only if the other has characteristic $p$ (including $p = 0$):

lemma ring_hom.char_p_iff_char_p {K L : Type} [field K] [field L]
  (f : K →+∗ L) (p : ) : char_p K p  char_p L p :=
  { introI _c, constructor, intro n,
    rw [ @char_p.cast_eq_zero_iff _ _ p _c n,  f.injective.eq_iff, f.map_nat_cast,
    f.map_zero] }

We see that the proof script splits the iff statement into each direction, but both directions are proved by the same tactic block. It is non-trivial to determine just by reading the proof given what the weakest assumptions possible are, and it is not immediately clear from the statement either. The meta-program determined these are that $K$ should be a division ring, and $L$ should be a nontrivial semiring.

Yury Kudryashov’s rotation number paper

Yury Kudryashov wrote a paper about the rotation number for the CICM 2021 conference on intelligent computer mathematics.

Rotation number is the key numerical invariant of an orientation preserving circle homeomorphism. Circle self-maps $f : S^1 → S^1$, $S^1 = ℝ/ℤ$, constitute an important class of dynamical systems. They appear in applications, e.g., as Poincaré maps of continuous flows on the $2$-torus. The simplest circle self-maps are pure rotations $x ↦ x + a$. It turns out that any circle homeomorphism f is semiconjugate to a pure rotation $x ↦ x + τ(f)$. The number $τ(f)$ is called the rotation number of $f$.

This paper describes the current state of an ongoing project with aim to formalize various facts about circle dynamics in Lean. Currently, the formalized material includes the definition and basic properties of the translation number of a lift of a circle homeomorphism to the real line. Yury Kudryashov also formalized a theorem by Étienne Ghys that gives a necessary and sufficient condition for two actions of a group on the circle by homeomorphism to be semiconjugate to each other.

Sébastien Gouëzel’s Gromov-Hausdorff Space paper

Sébastien Gouëzel wrote a paper about the Gromov-Hausdorff space for the CICM 2021 conference on intelligent computer mathematics.

The Gromov-Hausdorff space is the space of all nonempty compact metric spaces up to isometry. It has been introduced by Gromov, and plays now an important role in branches of geometry and probability theory. Its intricate nature of a space of equivalence classes of spaces gives rise to interesting formalization questions, both from the point of view of the interface with the rest of the library and on design choices for definitions and proofs.

Section 1 gives a purely mathematical description of the Gromov-Hausdorff space and its salient features. Section 2 gives an overview of the formalization. The last three sections are devoted to specific interesting points that were raised during this formalization. More specifically, Section 3 discusses the possible choices of definition for the Gromov-Hausdorff space. Section 4 explains how preexisting gaps in the mathlib library had to be filled to show that the Gromov-Hausdorff distance is realized. Section 5 focuses on a particularly subtle inductive construction involved in the proof of the completeness of the Gromov-Hausdorff space, and the shortcomings of Lean 3 that had to be circumvented to formalize it

This month in mathlib (Aug 2021)

This post summarizes some of the activity that happened in mathlib in August.

Highlighted PRs

  • PR #8652: chore(*): update lean to 3.32.1
    The community fork of Lean made two new releases 3.32.0 and 3.32.1. This is part of the preparations for porting mathlib to Lean 4.

  • PR #8281: continuous and smooth partition of unity
    See the companion blogpost for details.

  • Radon-Nikodym and Lebesgue decomposition. The four PRs PR #8645 PR #8687 PR #8763 PR #8875 together contribute the Lebesgue decomposition for sigma-finite measures and the Radon-Nikodym theorem.

  • PR #7978: strong version of FTC-2
    This weakens considerably the assumptions of part of the fundamental theorem of calculus: $\int _{a}^{b}f'(x)\,dx=f(b)-f(a)$, replacing continuity of $f'$ by the much more natural assumption of integrability.

  • PR #4885: general adjoint functor theorem: If $G : D ⇒ C$ preserves limits and $D$ has limits, and satisfies the solution set condition, then it has a left adjoint.

  • PR #8692: finite fields exist
    Most of this PR had been lying around for ages, but it was finally put together in mathlib. It shows the existence and uniqueness up to isomorphism of a finite field with cardinal $p^n$ for any prime number $p$ and positive integer $n$.

  • Among several PRs from the Dedekind project, the two most noteworthy are

    • PR #8530: ideals in a Dedekind domain have unique factorization
    • PR #8626: define the ideal class group
  • PR #8377: new file
    This PR defines the complex upper half plane, together with the $\mathrm{SL}_2$-action.
    Upcoming PRs will characterize the fundamental domain of the $\mathrm{SL}_2(\mathbb{Z})$-action.

Other mathematical contributions

The following PRs are ordered by the date that they were merged into mathlib.

  • PR #8424: prove that complex functions are conformal if and only if the functions are holomorphic/antiholomorphic with nonvanishing differential
  • PR #8560: Add the Kronecker product
  • PR #8388: signed version of the Hahn decomposition theorem
  • PR #8588: Smith normal form for submodules over a PID This PR is a step towards the classification of finite type modules over a PID.
  • PR #8266: Stieltjes measures associated to monotone functions
  • PR #8598: add definition and first lemmas about weak-star topology
  • PR #8639: prove Haar measure = Lebesgue measure on $ℝ$
  • PR #8558: add working definition of elliptic curve
  • PR #8538: add nilpotent groups
  • PR #8343: generalize inequalities and invariance of dimension to arbitrary rings
  • PR #8791: volume of a (closed) $L^∞$-ball
  • PR #8576: define exponential in a Banach algebra and prove basic results

Continuous partitions of unity

In PR #8281, Yury Kudryashov completed his work on continuous and smooth partitions of unity.

A continuous partition of unity on a topological space $X$ is a collection of continuous functions $f_i : X → ℝ$ such that:

  • the supports of $f_i$ form a locally finite family of sets, i.e., for every point $x$ in $X$, there exists a neighborhood $U$ of $x$ such that all but finitely many functions $f_i$ are zero on $U$;
  • the functions $f_i$ are nonnegative;
  • the sum $\sum_i f_i(x)$ is equal to one for all $x$.

While the above definition is completely standard, it is often useful to have a collection of functions that act as a partition of unity only on some part $s$ of $X$. In that more general case, we keep the above two conditions everywhere but ask that the sum in the last item equals one on $s$ and is less than or equal to one everywhere. This is encoded in the following Lean structure, from topology.partition_of_unity.

structure partition_of_unity (ι X : Type*) [topological_space X] (s : set X := univ) :=
(to_fun : ι  C(X, ))
(locally_finite' : locally_finite (λ i, support (to_fun i)))
(nonneg' : 0  to_fun)
(sum_eq_one' :  x  s, ∑ᶠ i, to_fun i x = 1)
(sum_le_one' :  x, ∑ᶠ i, to_fun i x  1)

The main result from that file is then the following existence theorem.

/-- If `X` is a paracompact normal topological space and `U` is an open covering of a closed set
`s`, then there exists a `partition_of_unity ι X s` that is subordinate to `U`. -/
lemma exists_is_subordinate [normal_space X] [paracompact_space X] (hs : is_closed s)
  (U : ι  set X) (ho :  i, is_open (U i)) (hU : s   i, U i) :
   f : partition_of_unity ι X s, f.is_subordinate U

Eric Wieser's scalar action paper

Eric Wieser wrote a paper about scalar actions in mathlib for the CICM 2021 conference on intelligent computer mathematics.

Scalar actions are everywhere in mathematics. There are so many of them that a given type can easily get several ones from different origins. For instance $ℤ$ acts on itself by left multiplication but it also has the $ℤ$ scalar action that every additive group has, by repeated addition or subtraction. In general those multiple actions can be proven to be equal, but type class inference needs definitional equality. So a great deal of care has been taken, by Eric and others, when setting up the algebraic hierarchy in mathlib.

The paper tells this fascinating story and is recommended for anyone interested in multiple inheritance handling in Lean 3 type class system.

Welcome to the Lean community blog!

This is our brand new blog where you'll be able to find news about what is happening in the Lean prover community. It will feature:

  • posts highlighting some new contributions to mathlib
  • news about ongoing projects such as the Liquid tensor experiment or the sphere eversion project
  • news about exciting developments in other proofs assistants
  • announcements of conferences and talks
  • some explanations of specific topics in a less formal context than the documentations
  • speculations about future developments or somewhat philosophical discussions

There is no predefined list of authors. Everybody can submit a pull-request with a post. If you are unsure whether your post will be welcome then don't hesitate to first discuss the topic of your post on Zulip before investing too much time writing it.