Differential geometry elaborators experiment (AI summary: Currently, differential geometry in Lean/mathlib requires very verbose boilerplate. Patrick Massot’s experiments show that custom elaborators can hide most of it, automatically inferring the TotalSpace.mk' wrapping and ModelWithCorners arguments. The community is invited to discuss whether to adopt this approach more broadly.)
Mathlib overview Categories are: General algebra, Linear algebra, Topology, Analysis, Probability theory, Geometry, Combinatorics, Dynamics, Data structures, Logic and computation.
Root directory of the mathlib4 GitHub repository for mathlib4:
It contains everything in the project: source code (Mathlib/), documentation files, configuration files, tests, scripts, etc.
Mathlib/ subdirectory inside the repository.
This contains only the Lean source files for the mathematical library itself: the actual definitions, theorems, and proofs organized into topic-based subdirectories (like Algebra/, Geometry/, etc.).
Mathlib/Geometry/Manifold
The manifold subdirectory in mathlib4.
Sebastien Gouezel,
Michael Rothgang,
Patrick Massot
are the
main people working on differential geometry. You can see the latest work
here:
https://github.com/leanprover-community/mathlib4/pulls?q=is%3Apr+label%3At-differential-geometry+
The main channels on which current mathematical formalization work gets discussed are:
A few recent topics on differential geometry:The above information on current work was provided by Heather Macbeth, also a main person working in differential geometry.
From Michael Rothgang: Although there's no "formalising differential geometry group" at the moment. Floris van Doorn, Sébastien Gouezel, Yury Kudryashov, Heather Macbeth, Patrick Massot, Oliver Nash and Winston Yin all have made big contributions.