We report on our experience formalizing diferential geometry with mathlib, the Lean mathematical library. Our account is geared towards geometers with no knowledge of type theory, but eager to learn more about the formalization of mathematics and maybe curious enough to give Lean a try in the future. To this efect, we stress the possibly surprising diference between the formalization and its pen-and-paper counterpart arising from Lean's treatment of equality. Our three case studies are Lie groups, vector bundles and the Lie algebra of a Lie group.
The logical system underlying the Lean theorem prover is known as an intensional dependent
type theory [
The singular “equality” in the title actually hides a plural. Indeed, there are multiple notions of equality in Lean, most notably the so-called definitional equality and the so-called propositional equality. Some traces of this distinction can be found in traditional mathematics with the “defined to be equal to” symbol := and with the non-trivial equalities stated as propositions which have to be proved. Unsurprisingly, two terms that are definitionally equal in Lean can be used interchangeably. In order to be able to refer to the equality between two terms within Lean’s syntax, there exists a second kind of equality, namely the propositional equality. However, if in pen-and-paper mathematics two expressions which have been proved equal can now be used interchangeably, blurring the above distinction, in Lean these two notions of equality are really distinct. Indeed, in Lean two terms that are propositionally equal may not be definitionally equal. For instance, the equality + 0 = is true by definition in Lean, while 0 + = is not and as a proposition requires a proof. Of course, definitional equality depends on implementation, something that mathematicians may not be used to take into account. After some work, implementation details can to some extent be abstracted away from the user, but they clearly afect the experience of the developer building an interface for a given mathematical structure. In pen-and-paper mathematics, mathematical structures are ethereal specifications without implementations and in the example above natural numbers form a totally ordered commutative semiring in which the definition of addition as such does not matter. We will see what kind of unexpected challenges these distinctions pose for the translation of pen-and-paper mathematics into Lean.
Manifolds in Lean are smooth manifolds locally modeled on a model with corners over a nondiscrete normed field k, i.e. a field equipped with a valuation, namely a real-valued map satisfying () = 0 if and only if = 0 and
() = () (), ( + ) ≤ () + () for all , ∈ k, and in which there exists an element with () < 1. The field k can be R together with the absolute value for instance and in this case in pen-and-paper mathematics -dimensional manifolds with corners are locally modeled on [0, ∞) × R− for some with 0 ≤ ≤ . If smooth manifolds without boundary and manifolds with boundary are well known, manifolds with corners are comparatively less known. Obviously, manifolds with corners generalize both boundaryless manifolds (case := 0) and manifolds with boundary (case := 1). While a nondiscrete normed field does not add much complication and allows to treat both real and complex manifolds at the same time, the set-up of manifolds with corners in Lean requires some formal machinery as we will briefly see below and using them may be cumbersome for the casual user. Beyond some basic material, as of June 2021 the Lean library for diferential geometry lacks more advanced material, like de Rham cohomology and Riemannian geometry, that could stress-test the design choices made. It will be interesting to follow the evolution of this library.
Smooth manifolds in Lean as formalized by Sébastien Gouëzel are modeled on a model with corners, denoted I : model_with_corners k E H in Lean. Given a model vector space and a model space , a model with corners is defined as a map : → embedding nicely into with respect to which the transition functions, which are maps from to , are smooth. In the case where k := R, one example of a model with corners is the embedding of [0, ∞) into R. In the trivial case where the map is the identity denoted id, embedding into itself, there is in Lean a trivial model with corners denoted model_with_corners_self k E. In the case of boundaryless manifolds we shall see the complications arising from Lean’s treatment of equality. In this case one would expect to work only with the trivial model with corners, but this is not the case. Indeed, assume that we have two model vector spaces and . There are two natural models with corners on × , namely the identity id and the product id × id, namely the map ( p : E × F, (p.1, p.2)), where p.1 and p.2 denote the first and the second projection, respectively. These two maps are not definitionally equal, hence we have to indicate to Lean which one we want to use. More precisely, the map id arises from considering × itself as a boundaryless manifold, while the map id × id arises from considering × as the product of two (boundaryless) manifolds, this product being denoted model_prod in the library. This exemplifies well the kind of subtleties involved with the equality in Lean. As a result, for boundaryless manifolds a dedicated property1 had to be introduced by Gouëzel. This property, simply ensuring that a manifold has no boundary, has an unspecified model with corners to maximize the applicability of its theorems.
In this subsection we will see in the case of Lie groups the consequences of the design choices for smooth manifolds outlined above. First, given the set-up of manifolds in Lean, a Lie group in Lean is a priori a manifold with corners. Second, in the case of Lie groups one would expect to use the trivial model with corners given by the identity map id, namely the model model_with_corners_self. However, the product of two manifolds and ′ in the library requires to use model_prod H H’ as the model space of × ′, where and ′ are the respective model spaces of and ′. As a consequence, using the trivial model with corners for formalizing Lie groups would not make Lie groups stable under products, i.e. it would not be possible to prove that the product of two Lie groups is again a Lie group. Indeed, assume that := and ′ := ′ are two Lie groups, each endowed with the trivial model with corners, hence (resp. ′) is (resp. ′) and both and ′ are id, then the product × ′ would be endowed with the model with corners id × id, which is not definitionally equal to id as explained previously, so × ′ would not be a Lie group if Lie groups were defined using the trivial model with corners. Thus, the definition of a Lie group has to be generalized, maybe awkwardly, allowing a model with corners where the model space and the model vector space can be distinct. We give below the code for our definition of Lie groups for the curious reader who wants to know what Lie groups look like in Lean, but we do not expect them to be able to make sense of the code. @[ancestor has_smooth_mul, to_additive] class lie_group {k : Type*} [nondiscrete_normed_field k] {H : Type*} [topological_space H] {E : Type*} [normed_group E] [normed_space k E] (I :
model_with_corners k E H) (G : Type*) [group G] [topological_space G] [charted_space H G] extends has_smooth_mul I G : Prop := (smooth_inv : smooth I I ( a:G, a− 1)) We then proceed to prove without any dificulty that the product of two Lie groups is again a Lie group.
One could define a vector bundle in Lean as a surjective continuous map : → satisfying standard conditions [3, chap. 3]. However, in case of a naive implementation of this definition the fibers of the tangent bundle would not be definitionally equal to the tangent spaces, only isomorphic to them. This is perfectly acceptable for the working mathematician, but now the Lean developer would have two isomorphic copies of the tangent space at a given point. As a consequence, our developer would have to transport theorems about these copies along an isomorphism, something which is never carried out explicitly on paper, since mathematicians treat isomorphic objects as equal. Thus, following a suggestion of Mario Carneiro we defined instead a topological vector bundle as a map E : B → Type*, i.e. a family of types, the fibers, indexed by a base space , such that each () is a topological vector space and around every point there is a local trivialization which is linear in the fibers. This definition of vector bundles has the merit of providing a more direct way of talking about fibers, avoiding to deal with fibers only isomorphic to tangent spaces. Thus, topological vector bundles translate into Lean as follows. class topological_vector_bundle (R : Type*) {B : Type*} (F : Type*) (E : B → Type*) [semiring R] [∀ x, add_comm_monoid (E x)] [∀ x, module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (total_space E)] [topological_space B] : Prop := (inducing [] : ∀ (b : B), inducing ( x : (E b), (id ⟨b, x⟩ : total_space E))) (locally_trivial [] : ∀ b : B, ∃ e : topological_vector_bundle.
trivialization R F E, b ∈ e.base_set)
2.3.1. Derivations of the Algebra of Smooth Functions on a Manifold We already touched on the isomorphism-as-identity problem in the previous section. We will give one additional incarnation of this problem to exemplify how pervasive it is in the formalization of mathematics with proof assistants. Given a real smooth manifold , it is known2 that Der(∞( )), the real vector space of derivations of the algebra ∞( ) of smooth functions on , is isomorphic to Γ ∞(, ), the real vector space of smooth vector ifelds on .
Γ ∞(, ) ∼= Der(∞( ))
This isomorphism is an isomorphism in the category of Lie algebras over R. Since derivations of
the algebra of smooth functions is a more algebraic theory, it is particularly well suited for the
dependent type theory of Lean and we chose to follow this approach as shown in the snippet of
code below.
2Cf. https://ncatlab.org/nlab/show/derivations+of+smooth+functions+are+vector+fields
@[protect_proj]
structure derivation (R : Type*) (A : Type*) [comm_semiring R] [
comm_semiring A]
[algebra R A] (M : Type*) [add_cancel_comm_monoid M] [module A M] [
module R M]
[is_scalar_tower R A M]
extends A → [R] M :=
(leibniz’ (a b : A) : to_fun (a * b) = a · to_fun b + b · to_fun a)
However, in some situations one might prefer to work with vector fields and even once the
above isomorphism has been proved, it would remain to transfer along the isomorphism
properties from one side to the other and this would not be handled automatically by Lean.
This is a significant diference between Lean and the practice of pen-and-paper mathematics
where isomorphic objects are treated as equal. It is worth noting that in some dependent type
theories like Voevodsky’s Univalent Foundations [
pi.smul_apply] } }
There are hints that the approach taken for formalizing manifolds in Lean is scalable, though much remains to be done to extend the library which currently lacks an array of nontrivial examples for the notions already implemented. Regarding Lean itself we have to point out that the level of automation is not on a par with what most mathematicians would expect. Moreover, the fact that every term belongs to a type creates some dificulties that a mathematician will hardly suspect. Indeed, if Lean type class inference mechanism allows to see automatically a Lie group as a group or a Lie group as a smooth manifold, one needs the so-called coercions to see for instance a smooth map as a map. These coercions clutter the code and render it unnecessarily verbose from the mathematician’s perspective always equating an object with its image under a forgetful functor or a canonical inclusion. A mathematician may also regret the limited support for notations that makes the code verbose and hard to decipher as well as the absence of LATEX support to comment extensively the code with formulas or diagrams. Also, given its sophisticated type theory Lean has problably a steep learning curve for most mathematicians and the cryptic messages given in the user interface whenever an error occurs are not of much help to the beginner. Finally, if mathematicians think they know what equality is, implementing their favorite mathematical structures in Lean may force them to revise this position.
This work was supported by the ERC Advanced Grant ALEXANDRIA (Project GA 742178) and the Cambridge Mathematics Placements Programme from the Faculty of Mathematics of the University of Cambridge. We thank the maintainers of mathlib, as well as Oliver Nash, who took an active part in reviewing our code after it was submitted to mathlib. Among the mathlib maintainers we thank in particular Sébastien Gouëzel. We also thank one anonymous reviewer for their relevant remarks.
• Lie groups, • Topological vector bundles, • Lie algebra of a Lie group.