looking for advice on choosing a formalization project

Stream: mathlib4

[Michael Novak]

Hi, I'm looking for advice from experienced mathlib contributors before choosing a subject for a formalization project to contribute to mathlib. Before getting into details, I just wanted to make sure - is this channel an appropriate place to ask that?

[Michael Novak]

So, I've been studying lean for about 3 months mainly from the math in lean textbook, but also from the theorem proving in lean 4 textbook and also a bit from the functional programing in lean textbook. I've also been interested in foundations in general in the past, I have a decent backgrounds in classical mathematical logic and set theory and I learned on a basic level about type theory from the first chapter of the HoTT book and I've learned on a basic level about the lambda calculus and the Curry-Howard isomorphism from the first few chapters of the book "Lecture notes on the Curry-Howard isomorphism". So at this point I feel like I have a decent understanding of naive type theory and the basics of lean, or at least decent enough for the sort of formalization project I want to write, and I also plan to continue learning lean when I start working on the project.

What I wanted to do is formalize some important result, that doesn't exists yet on mathlib to contribute to the library. I wanted to ask the experienced contributors of mathlib for suggestions for an appropriate subject / specific theorem to formalize based on the following criteria:

1. Considering my background in lean and type-theory as I described it in the first paragraph, I would like the project to take about 50-70 hours in total, including all the needed definitions and lemmas. I know it's probably hard to estimate such a thing, it's totally fine if your estimation wouldn't be very good, but I would appreciate if you could estimate that to the best of your ability based on your experience.
2. The subject I would like the project to be on is from one of the following possible subjects:

   - (abstract) linear algebra - anything from either K.Hoffman, R.Kunze Linear Algebra, or Linear algebra done right by Axler.
   - Multivariable analysis and possibly basic analysis on manifolds: specifically anything from the first 5 chapters of the book "Analysis on Manifolds" I already know and also other typical multivariable analysis material which doesn't appear there - like the second derivative test and Lagrange multipliers, and I'm going also to learn the rest of the book, so if there's something there that you think could be a good subject, I have no problem starting to learn it now earlier.
   - Elementary differential geometry - I'm taking a course about this subject right now - so I don't yet know all the material, but I absolutely love this subject. We are using these 3 books: "Elementary differential geometry" by Christian Bar, "Differential Geometry of Curves and Surfaces" by Do Carmo and "Differential Geometry of plane curves" by Alencar, Santos and Neto. I really love this subject and I don't mind studying a bit ahead to learn some result that could be good as a subject for the project.
   I should also say that I know that many of the results of these subjects have generalizations, and maybe in mathlib you prefer to prove the most general results, but unfortunately I probably don't have enough background to prove everything in the most general settings, so take that into consideration, and also if you think it would be very easy for me to learn some generalization of a result, I'm totally open to that as well.

So that's it pretty much. I would love to hear from you any suggestions that you think could be fitting.

[Floris van Doorn]

Yes, this is a good channel to ask this. This thread may be relevant: #general > List of good undergraduate projects

[Michael Novak]

Floris van Doorn said:

Yes, this is a good channel to ask this. This thread may be relevant: #general > List of good undergraduate projects

Thanks! I looked through this thread and saw your LeanCourse project tips - I definitely think this could help me when I will start working on the project, but I didn't find there a topic that I thought could be good for me. I also saw this list: https://leanprover-community.github.io/undergrad_todo.html - some of the topics in this list seems good for me, but some of them are very general - like 'partial derivatives' or 'diagnolization', so I'm not sure what exactly is missing from mathlib - is it like everything about it missing - including basic definitions? It's hard to imagine that's the case since there are much more advanced topics formalized in mathlib, that I would imagaine use these basic definitions. The other problem is that I have no idea how hard are some of these topics to formalize and will they fit the scope of the project I want to make (not too big, not too small), that's why I wanted to ask here experienced mathlib contributors. Also in this thread you sent I saw that Kevin Buzzard said that this list may not be good for undergrads.

[Ben Eltschig]

There was also a thread about projects specifically in differential geometry recently here: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Looking.20for.20Differential.20Geometry.20Project/with/555708054

[Michael Rothgang]

Indeed, "undergrad mathematics not yet in mathlib" is not a good fit for beginning formalisations projects. All these notations are still on that list for a reason (mostly to do with "what's the right generality to define them in" and "we don't use them that often in practice" --- mathlib so far got by very well without a definition specifically for partial derivatives), and making progress on them without knowing mathlib well is not going to be useful.

[Michael Rothgang]

Differential geometry can indeed use quite some help. The projects I mentioned in the thread above are for the general case (n-dimensional manifolds, not curves or surfaces). A more approachable topic could be one specifically for 2 or 3d: for instance, what do you think about Frénet's equation in 2d or 3d?

[Michael Rothgang]

(Once we have the general definition of curvature in mathlib, we definitely want to relate the curvature of parametrised curves in R² to the general definition --- but we surely want the simpler expression as well, so working on this would not be wasted work.)

[Michael Novak]

Michael Rothgang said:

Differential geometry can indeed use quite some help. The projects I mentioned in the thread above are for the general case (n-dimensional manifolds, not curves or surfaces). A more approachable topic could be one specifically for 2 or 3d: for instance, what do you think about Frénet's equation in 2d or 3d?

That actually sounds like a great idea!

[Michael Rothgang]

Let me add that these formulas also exist in n dimensions. Depending on your motivation, you can also do these...

[Michael Novak]

Michael Rothgang said:

(Once we have the general definition of curvature in mathlib, we definitely want to relate the curvature of parametrised curves in R² to the general definition --- but we surely want the simpler expression as well, so working on this would not be wasted work.)

So there isn't any problem if I define curvature for plane parametric curves, even though there is a more general definition of curvauture, right?

[Michael Rothgang]

I think this should be fine: long-term, we want to define curvature more generally and show the 2d expression agrees with it. In your formalisation, perhaps you can try to never unfold your definition of curvature, but always rewrite by a lemma says "the curvature is equal to this", where "this" is what your definition will be. That statement should remain true, and make it easy to adapt in the future.

[Michael Rothgang]

We sadly don't have good introductory resources to differential geometry yet. This file mentions a very very few things; I will be teaching an updated and extended version in early January (and a 30 minute version in two weeks). If you like to be a guinea pig, I can certainly share early versions of these with you beforehand.

[Michael Novak]

Michael Rothgang said:

We sadly don't have good introductory resources to differential geometry yet. This file mentions a very very few things; I will be teaching an updated and extended version in early January (and a 30 minute version in two weeks). If you like to be a guinea pig, I can certainly share early versions of these with you beforehand.

I'm not sure if I have the right background to understand this. Sorry if this is a stupid question, but why do think this could help my relatively elementary project to know about how more advanced and general differential geometry is done in mathlib? I think that I will need to use in my project mostly linear algebra and real analysis, am I'm missing something?

[Michael Novak]

Anyways, thank you very much for the topic idea!

[Oliver Nash]

The Cayley–Dickson construction and the octonions are missing and would be a very accessible and useful project.

I know @Filippo A. E. Nuccio previously supervised a lovely project in which these were done but they never made it to Mathlib.

[Filippo A. E. Nuccio]

Indeed, I supervised a project in which these were done but the code never made it to Mathlib. @Michael Novak In case this is of interest to you, do not hesitate to DM me!

[Michael Novak]

Thank you very much for the suggestion and proposal for supervision! I looked in Wikipedia about this topic because I wasn't familiar with it, it looks very interesting, but I prefer to choose a topic from the areas I mentioned above. Maybe this could be a cool project I will do in the future. Btw, why did the code never made it to Mathlib?

[Filippo A. E. Nuccio]

Sure, no problem! It is a wise choice to pick up a subject that you like, since the formalisation process might be painful, so better loving the topic! It did not make it to Mathlib because I supervised it during a summer school, and eventually all participants went back to their institutions and nobody worked hard enough to polish the code to make it Mathlib-compatible.

[Yan Yablonovskiy 🇺🇦]

Filippo A. E. Nuccio said:

Indeed, I supervised a project in which these were done but the code never made it to Mathlib. Michael Novak In case this is of interest to you, do not hesitate to DM me!

Out of curiosity , was the previous project in Lean 4 or 3?

and is the offer open to others :nerd:

[Filippo A. E. Nuccio]

It was lean 4, and of course the offer is open to everyone!

[Michael Rothgang]

Ah right, you consider parametrised curves from the real numbers to Euclidean space :man_facepalming: In that case, you indeed don't need to know about manifolds.