What definitions are missing in mathlib?

Stream: mathlib4

[Kevin Buzzard]

I am becoming more and more convinced that missing definitions are a major bottleneck for growth. Definitions are not at all easy. For example, yesterday I exchanged around 200 DMs with a group of people on the subject of just one basic Masters level definition, and there is still more to talk about (and possibly a refactor).

In my Big Proof talk I listed the following missing definitions which we'll need to get (my proposed route to) FLT over the line (and I've tidied up/clarified the list a bit):

Group homology, Tate cohomology (of finite groups), continuous cohomology,
local fields, fundamental characters, the Artin map,
elliptic curves over schemes,
abelian varieties, moduli spaces in algebraic geometry,
Shimura varieties, etale
cohomology, fppf cohomology, algebraic de Rham cohomology,
classical de Rham cohomology,
$L$-functions of modular curves and elliptic curves, automorphic forms
and automorphic representations for $GL_2$
and quaternion algebras, real/complex manifold associated to
a smooth (connected) real/complex algebraic variety,\ldots

The list is out of date -- group homology is now merged! But this list is highly skewed. I'm giving a talk tomorrow to a maths department and I wondered if I could get a more balanced list. What is missing from other areas of maths? Things that sprung to mind are: knots, Riemannian manifolds, symplectic manifolds. But there must be plenty more. I am specifically interested in things which are commonly-used by research mathematicians in mathematics departments (because this is a talk for research mathematicians in a mathematics department). What are other obvious examples of definitions which we don't have but surely need?

[Yaël Dillies]

Contour integrals? :grinning:

[Luigi Massacci]

Distributions (in the analysis sense), and I guess currents too.

[Robin Carlier]

Spectras (in the stable homotopy theory sense).

[Sébastien Gouëzel]

Riemannian manifolds are on their way, see #25347 (currently stuck on #25383, will need many other PRs)

Distributions are essentially there (we have the Schwartz space as a topological vector space, and dual spaces) -- they haven't been used seriously, but as far as definitions are concerned everything is there.

[Luigi Massacci]

Sébastien Gouëzel said:

Distributions are essentially there (we have the Schwartz space as a topological vector space, and dual spaces) -- they haven't been used seriously, but as far as definitions are concerned everything is there.

I meant non-tempered distributions. Though I agree that since WithSeminorms is very developed, a lot of the stuff is there to define distributions over test functions / compactly supported distributions, etc. But then again it's been there since 2023 : )

[Filippo A. E. Nuccio]

Sobolev spaces

[Riccardo Brasca]

Abelian varieties

[Bryan Gin-ge Chen]

Connections on fiber bundles

[Yaël Dillies]

Genus of a curve

[Filippo A. E. Nuccio]

Octonions (although we gave it a go in Leiden, but it never made to Mathlib)

[Rémy Degenne]

The Itô integral

[Michael Rothgang]

does "Brownian motion" count? (which is in progress also)

[Michael Rothgang]

differential forms (implicit in your list above)

[Michael Rothgang]

geodesics and the exponential map (in Riemannian manifolds)

[Anatole Dedecker]

Tensor product of bimodules over noncommutative rings :upside_down:

[Michael Rothgang]

submanifolds (of topological/smooth manifolds) --- working on them

[Ben Eltschig]

Topological groupoids and Lie groupoids are something I'd like to see. We had a thread about groupoid objects here a few weeks ago - that would be half of the puzzle, the other would be some suitable category of smooth manifolds to apply that to

[Ben Eltschig]

I was also going to say pro-objects, but I'm unsure if we have that already - we have docs#CategoryTheory.Ind, but I can't find a dual counterpart

[Kevin Buzzard]

Yeah I don't think we have pro-objects. Two cool theorems about them: pro(finite sets) is equivalent to profinite sets, and pro(Artin local rings) is (I think) pseudocompact rings (something which would be nice to have for FLT if it's true).

[Robin Carlier]

Well, there’s (Ind Cᵒᵖ)ᵒᵖ...

[Robin Carlier]

(To be clear, this is a joke and we should definitely have infrastructure for pro-objects)

[Kevin Buzzard]

We should have a tactic which makes it from the Ind case! But people have tried before...

[Kevin Buzzard]

Yaël Dillies said:

Contour integrals? :grinning:

I think we have contour integrals? It's just that we don't have the most obvious theorem about them, right?

[Andrew Yang]

Probably will skew your list more but
Rigid analytic space/Berkovich space/adic space
Cartier divisors, line bundles, intersection pairing, chern class, chow ring
birational maps, blow ups, minimal models
(ruled/elliptic/del Pezzo/K3) surfaces

[Anatole Dedecker]

Amenable topological groups, property T, convolutions on a locally compact group, C*-algebras of a locally compact group

[Michael Rothgang]

Riemann surfaces (though perhaps we just don't have their properties)

[Michael Rothgang]

Fundamental class of e.g. a manifold

[Kevin Buzzard]

I thought we had manifolds which were locally modelled on $\mathbb{C}$. Isn't this exactly Riemann surfaces?

[Anatole Dedecker]

K_0 of a ring (and hence of a topological space)

[Robin Carlier]

K_n of a Ring :D

[Michael Rothgang]

Kevin Buzzard said:

I thought we had manifolds which were locally modelled on $\mathbb{C}$. Isn't this exactly Riemann surfaces?

We do. "1-dim complex manifold" is only part of the story - perhaps the rest is a theorem

[Michael Rothgang]

Partial differential operators

[Michael Rothgang]

their principal symbol

[Anatole Dedecker]

Robin Carlier said:

K_n of a Ring :D

Well then, K_n of a Banach algebra x)

[Damiano Testa]

Surely in mathlib that would be K_n of a [Add X].

[Kevin Buzzard]

I've gone with "K theory", I think that covers everything :-)

[Ben Eltschig]

Topoi and quasitopoi would also be nice to have. We do already have topoi at least in the sense that we have finitely complete and cartesian-closed categories as well as subobject classifiers, but I think for quasitopoi we're still missing regular / strong subobject classifiers completely

[Anatole Dedecker]

(My point in saying K_0 is that this one is the same for everyone, which isn't true of the higher K_n's -- the one I care about is 2-periodic!)

[Kevin Buzzard]

my point is that we don't have any of them :-)

[Ruben Van de Velde]

Can we say we have "graphs" yet? I guess "depends on what you want a graph to look like"

[Kevin Buzzard]

Yeah we have one of them :-)

[Scott Carnahan]

Most of the key notions in “Sphere packings, lattices, and groups” are still missing, e.g., Golay codes, hexacode, lattice genera, Niemeier lattices. A lot of it is focused on exceptional structures, but there is also missing theory.

[David Ledvinka]

Markov Chains / Markov Processes

[Aaron Hill]

Matrix eigenvalues (without being limited to just Matrix.IsHermitian)

[Fred Rajasekaran]

I'm from probability so here's a list of some probability concepts I'd like to see eventually!

• Empirical probability measures and related concepts. Though I'll try to implement these as part of a random matrix theory Lean project this summer.
• On the topic of random matrix theory, the Stieltjes and Cauchy transforms and related concepts
• Gibbs measures (also in progress)
• Related to the above, but basically all the statistical mechanics lattice models (Ising model, Potts model, phi-4 model, percolation, lattice gauge theory, spin glasses, etc.)
• Large deviations (good rate function, large deviations principle, etc.)
• Free probability (*-probability space, free semicircular/poisson distribution, freeness/free independence, asymptotic freeness, etc.)
• Wasserstein distances and spaces, Wasserstein gradient/flows
• Monge-Kantorovich formation of optimal transport
• Message passing algorithms and related concepts (belief propagation)
• Stein Discrepancy/Kernel
• Random Graph models (ER random graph, stochastic block model, random geometric graph, random d-regular graph, etc.) (not sure if some of these are already in it)
• As mentioned above markov processes, markov generators
• Also mentioned above, brownian motion and Ito integral
• White noise, Gaussian free field (ideally fractional gaussian fields and forms)
• Functional inequalites (Log-Sobolev, Poincare, HWI, Talagrand)

I'm probably missing a bunch too :sweat_smile:

[Moritz Firsching]

Oriented matroids/hyperplane arrangements/polytopes

[Moritz Firsching]

Bordism as a homology theory

[Jihoon Hyun]

Oriented matroids

I'm struggling on formalizing this. I need some research on how to define 'infinite' oriented matroids which is relatable with the current implementation of Matroid. However the most reliable definition of infinite oriented matroid I could find is as noted in 'Oriented Matroids' by Bjorner et al, which I don't think is relatable with B-matroids. If someone's interested, maybe we can talk about it in this thread

[Michael Rothgang]

Moritz Firsching said:

Bordism as a homology theory

I worked in this direction (and there remains lots to do). Help welcome/I'm happy to mentor people!

[Wrenna Robson]

Scott Carnahan said:

Most of the key notions in “Sphere packings, lattices, and groups” are still missing, e.g., Golay codes, hexacode, lattice genera, Niemeier lattices. A lot of it is focused on exceptional structures, but there is also missing theory.

Indeed, I think there is very little coding theory (which I suppose you could view as a subset of this kind of thing, but I guess it depends on perspective).

[Wrenna Robson]

If you count cryptography as mathematics (perhaps arguable), there's a bunch of cryptographic concepts missing.

[Dagur Asgeirsson]

Stable $\infty$-categories

[Martin Dvořák]

NP

[Kalle Kytölä]

Kevin Buzzard said:

Yaël Dillies said:

Contour integrals? :grinning:

I think we have contour integrals? It's just that we don't have the most obvious theorem about them, right?

I think Yaël is right in counting contour integrals as missing. Of course in the case of a $C^1$-path $\gamma : [a,b] \to \mathbb{C}$ one can define this as $\int_\gamma f(z) \, \mathrm{d}z := \int_a^b f\big( \gamma(t) \big) \, \gamma'(t) \, \mathrm{d}t$ like is done in docs#circleIntegral, and one could still do the same for piecewise $C^1$ paths. But if path homotopy is to be done in the continuous category $C^0$ (as it clearly should be, right?), then even for stating the homotopy invariance of contour integrals we don't have a definition.

The issue is that there are two separate generalizations of $\int_\gamma f(z) \, \mathrm{d}z$ from (piecewise) $C^1$ paths $\gamma$ and holomorphic functions $f$:

• One can allow $f$ to be more general, certainly any continuous $f$ (or measurable + something that guarantees integrability) is ok as long as $\gamma$ is (piecewise) $C^1$ path (rectifiable $\gamma$ could be ok, still, but the point is that some regularity must be assumed on $\gamma$; homotopy in $C^0$ category cannot be done).
• One can allow $\gamma$ to be arbitrary continuous path as long as $f$ is holomorphic, because then the 1-form $f(z) \, \mathrm{d}z$ is locally exact (a.k.a. closed) and the integral can be defined (by local primitive, i.e., writing $f(z) \, \mathrm{d}z$ locally as $\mathrm{d}(F(z))$).

The latter generalization is needed to do the homotopy invariance of contour integrals of holomorphic functions. @Vincent Beffara had this definition in his proof of the Riemann Mapping Theorem, but as far as I can tell, it is missing from Mathlib.

This has been discussed many times, and I think the last bigger discussion lead to progress in homotopy. (Sorry, don't have the links at hand.)

[David Ang]

Do we have reductive groups?

[Joël Riou]

Kevin Buzzard said:

I've gone with "K theory", I think that covers everything :-)

Not in mathlib yet, but I have already formalized Quillen's Q-construction... https://github.com/joelriou/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/ExactCategory/Q.lean

[Kevin Buzzard]

(I've given the talk now BTW but I'm finding this thread very interesting so please feel free to continue :-) )

[Filippo A. E. Nuccio]

And what did you end up mentioning, @Kevin Buzzard ?

[Kevin Buzzard]

Screenshot 2025-06-18 at 22.41.54.png

[Scott Carnahan]

I haven’t seen any Ricci/sectional/Riemann curvature.

[Jz Pan]

I'm curious if these can be organized into a dependency graph.

[Kevin Buzzard]

The idea in the talk was that most of these were "we don't have this, but we have a lot if not all of the prerequisites so we could start working on it tomorrow, and actually some people are already working on some of these"

[Dominic Steinitz]

Scott Carnahan said:

I haven’t seen any Ricci/sectional/Riemann curvature.

Or connections