Differential geometry problems for undergrad final project?

Stream: maths

[Gavin Zhao]

I'm taking an undergraduate differential geometry course and now it's the time to consider a final project. I want to do a formalization of a theorem in Lean as the project.

Are there any differential geometry theorems in Mathlib that would be suitable for an undergraduate math student to prove?

As for my skill level, I've only been using Lean extensively for PL-related (language semantics and compiler optimization) proofs, but I've never written or used a Lean proof that is even remotely related to calculus.

My professor provided a list of potential theorems to choose from, but obviously this is for students that are not doing formalization and may or may not be too difficult to do in Lean:

1. Compact + constant Gauss curvature implies spherical (do Carmo 5.2)
2. Isoperimetric inequality (do Carmo 1.7)
3. Four vertex theorem (do Carmo 1.7)
4. Crofton length formula (do Carmo 1.7)
5. Fundamental theorem of surfaces (do Carmo appendix to Section 4)
6. Hopf-Rinow theorem (do Carmo 5.3)
7. Differentiable Jordan curve theorem (do Carmo 5.7)
8. Fenchel’s theorem/total curvature of plane curves (do Carmo 5.7)
9. Knotted curves and the Fary-Milnor theorem (do Carmo 5.7)
10. Abstract definition of a Riemannian surface (do Carmo 5.10)
11. Gauss linking formula
12. Fundamental theorem of curves in higher dimensions

Thanks in advance!

[Xinyi Zhang]

The Jordan curve theorem came up when discussing the cohomology axioms. It could be of value to the current developments in cobordism if that theorem was formalized.

[Michael Rothgang]

Thanks for asking; let me think about this. I'm quite busy with teaching today - if you don't hear from me by tomorrow, feel free to send me a reminder in a DM!

[Michael Rothgang]

In short, if your goal is "fully formalise X and all of its prerequisites", you should aim much smaller. Or your project should be "let me assume X and Y, now prove Z".

I'll write more details later!

[Michael Rothgang]

I'll have to run in 10 minutes, but let me give some detail already (on what mathlib knows and does not).

• in general, differential geometry is tricky to formalise. (For each area, you need to find the right tricks to make that nice, and we have found some tricks, but are missing one or two. So, don't despair if it's hard and feel free to ask for help!)
• if you want to formalise a topic, you should know the mathematics really really well. Lean will turn up questions you didn't think about (that also happens for me!).

[Michael Rothgang]

About suitable topics: a lot of basic differential geometry material is already there, but a lot is also missing: for several projects above, you may need to assume some properties to make them doable. To start:

• we have Riemannian manifolds, the Levi-Civita connection (in a branch of mathlib - you could copy our code and move on), but not the curvature tensor yet. So even stating "constant Gauss curvature" is tricky.
• we don't have geodesics yet (and they are not far, but doing them right is probably not a good first project)
• we don't quite have submanifolds yet, but are close: I have a branch of mathlib containing them.

[Michael Rothgang]

When do your formalisation projects start? Is working on a branch of mathlib an option? (If so, I could try and make a branch containing "all the differential geometry prerequisites you'd like to have, that are still being reviewed and not in mathlib yet".)

[Michael Rothgang]

If your project involves the Levi-Civita connection, submanifolds (or both), be aware that you will find lots of basic lemmas about them that are missing (simply because nobody proved them yet). Doing so would be very nice, though.

[Michael Rothgang]

So far for now, I have to run...

[Moritz Doll]

I would guess that the only item on your list that I would expect to be feasible a complete formalization would be the four vertex theorem.

I would rule out everything with surfaces (we have definition of abstract manifolds as Michael indicated, but relating that to surfaces and doing the simplifications is probably very tedious and not mathematical insightful). That leaves basically the isoperimetric inequality, four vertex, Cauchy-Crofton, and differentiable Jordan curves. Jordan curves seem to need Gauss-Bonnet, which relies on knowing what curvature is, so that is a no in mathlib. The isoperimetric inequality needs a formula for the area, which is a consequence of Green's theorem (which we do not have), however just assuming that formula might make it possible. The proof of Cauchy-Crofton is rather hand wavy (I think it only proves it for a straight line and then "use a limiting argument"), so also not great for formalization.

[Gavin Zhao]

@Michael Rothgang Thanks a lot for the very detailed response! This is my first time dealing with the "math" part of Lean so those advice are very helpful.

The project technically starts next week. However, right now I'm still investigating what I want to formalize (and whether a formalization project is feasiable at all) so I don't want you to spend time making the branch and then I proceed to not use most if not all of it :sweat_smile: I will let you know if I need any help from you!

[Gavin Zhao]

I'll give four vertex theorem a look. Thanks @Moritz Doll!

[Gavin Zhao]

The professor is not very strict on how "rigorous" the formalization is (i.e. it's ok to assume some very tedious/inconvenient stuff and it doesn't have to be a publish-able result), so I'm not worried about targeting a fork/branch of Mathlib. It's more so that I also have other final projects going on and I need to weigh how much time and effort I want to spend on this.

[Michael Rothgang]

Great that my answer was helpful! Right now, mathlib is at this unfortunate stage where many ingredients for interesting projects are still being worked on (connections, the Levi-Civita connection, geodesics, submanifolds, differential forms). I hope the situation will be better in half a year (but that doesn't help you now).

I have two or three further suggestions for projects you could probably do.

• If you like building basic theory, we don't have quotients of manifolds yet. Given a manifold M and a free and proper action* by a discrete group (e.g., Z_2 or the integers), the quotient is a manifold again. The motivating example is real projective space, which is a quotient of the sphere. The project could be to prove, in general, that such a quotient is a manifold, that the projection map is smooth and related facts (e.g., the projection is a local diffeomorphism).
• Prove that a diffeomorphism between connected manifolds is either orientation-preserving or orientation-reversing (copy-paste the definition of orientable manifold from Mathlib PR #16239 and assume your manifolds have no boundary).
• Define differential 1-forms and exact 1-forms (closed 1-forms are harder to define). Show that on a simply connected domain, every 1-form is exact. (We're still waiting for the general definition of n-forms to get merged into mathlib, but for this project, a "by hand" definition is perfectly fine.)

\* Some books call this a "properly discontinuous action", though this terminology is ambiguous.

[Michael Rothgang]

In any case, good luck with your decision!

[Michael Rothgang]

(And note that I'm preparing a branch with "all the submanifold stuff" anyway for a student I'm supervising, so additionally making one to include Levi-Civita would not be too onerous.)

[Kevin Buzzard]

Michael Rothgang said:

Right now, mathlib is at this unfortunate stage where many ingredients for interesting projects are still being worked on (connections, the Levi-Civita connection, geodesics, submanifolds, differential forms).

FWIW I felt 18 months ago that mathlib was at an unfortunate stage where many things needed to prove a certain finiteness result in the theory of automorphic forms were still being worked on (or indeed not even started but it was pretty clear how to do them), and then I gave a graduate course on the proof, which turned into these chapters here and here and here in the FLT blueprint. People worked on these in the FLT repo, even though all this stuff was well-known in the 1980s, and we have nearly got a complete proof of the finiteness result, which I think will turn into a nice paper.

On reflection I think that having the LaTeX was a great help to allow people to contribute; I didn't even write the Lean statements for some of the argument, people just came along and did that for me (statements and proofs). The problem with this idea: the proof is not in mathlib, and upstreaming is a different problem.

But I wonder whether one could avoid this problem by running a "blueprint only" project, where an expert such as yourself Michael writes down some basic goal in the area which will inspire development of what is needed and is probably paper-worthy (by the way, I have heard that AFM likes papers which have a well-defined "end goal" result, rather than "we develop more of this theory"), then writes down some blueprint chapters describing the mathematics, but then does not create an independent repo and instead runs the entire thing via mathlib PRs.

My guess is that if someone puts in the effort to get the LaTeX over the line, explaining exactly what is missing in mathlib, then you will find contributors; there are plenty of people around here who are interested in differential geometry in general and want to contribute. If there are difficult design decisions to be made then that's fine, the project can be a driver towards making those difficult design decisions. By far the most difficult design decision I have ever been involved in is figuring out how to define nonarchimedean local fields in Mathlib; this discussion took around two years, even though mathematically the various definitions are completely unambiguous and all equivalent. I am convinced that one of the major drivers of the fact that the definition actually went from "something we occasionally have Zulip threads about" to docs#IsNonarchimedeanLocalField was the fact that the class field theory blueprint exists and it got a bunch of people thinking about the problem, experimenting, and ultimately making a decision.

[Ruben Van de Velde]

I would note that collaborating as a group working towards a specific is likely to be harder with a mathlib-first approach, unless you have some maintainers who are able to get things merged very quickly

[Damiano Testa]

This also means that if the maintainer in question does not actually write the lean code, but just the blue-print, then merging PRs produced with code inspired by the blue-print would be uncontroversial, whereas merging a PR for which you also wrote a substantial part of the code would require a different maintainer to approve...

[Michael Rothgang]

@Kevin Buzzard Thanks for the suggestion. So far, I haven't dreamt big with "take a nice theorem and propose a blueprint formalising it". Perhaps I should change that (say, sometime next year) :-)

[Michael Rothgang]

Let me note, however, that the situation with connections, Levi-Civita, submanifolds or basics of bordism theory is mostly different: there, the work is "mostly" finished and by far the biggest bottleneck is getting reviews to hammer out the design and get things into mathlib. (#28793 blocks all of submanifolds, for instance --- I'll address the comments there later this week.)

[Michael Rothgang]

For differential forms, a large part of the work is upstreaming (Yury's PRs would be happy about more review), and at some point filling in the last sorries.

[Kevin Buzzard]

I think that mathlib-first should be something we experiment with more, now we have the Initiative.