What should I contribute to mathlib?

Stream: new members

[Martin C. Martin]

Hi, I've been learning Lean, and am more-or-less ready to start contributing to mathlib. Or at least to look into a first project and see what's involved. :) What's a good topic? What's an area or theorem I could contribute?

[Alex J. Best]

What are your (mathematical or compuitngy) interests, there are many possibilities of things to work on and it's always easier when it's an area you know well or are interested in looking at deeply

[Kyle Miller]

One algorithm is choose some theorem that interests you, start formalizing it with no intention of contributing it to mathlib, and then accumulate lemmas or other theory that are missing from mathlib as you work on this theorem. Then you polish these up, getting input from the community for how to structure them in a mathlib way, and then contribute these.

[Martin C. Martin]

I have about 2 or 3 years of an undergraduate program in math, from around 1990. Although I'm happy to learn anything I need. For computing, well I have a Ph.D. and was a professional software engineer for many decades. :)

For mathematical interests, either real or complex analysis, or abstract algebra. How much of that is formalized?

[Kyle Miller]

You could check the overview (which we try to keep updated)

[Martin C. Martin]

Which theorems aren't yet formalized? I assume e.g. all of the core of Spivak's Calculus is in mathlib? What about calculus on mainfolds?

[Kyle Miller]

There's an undergraduate todo list too, though beware that a number of things here remain because of technical challenges or unfinished long-discussed developments.

[Kyle Miller]

Here's a project that would benefit both mathlib and people learning Lean: choose a textbook like Spivak's Calculus, then go through it and try to prove everything in it with Mathlib. Importantly, give the theorem statement in as close to a Spivak-like way (with any concessions you need to make due to formalization of course), but then try to prove everything with pre-existing theorems.

There are bound to be gaps.

[Kyle Miller]

A reason I think people should do this sort of textbook translation is that then either (1) people can use the formalized textbook as a library for their own work or (2) use the formalized textbook as a rosetta stone to see what's the mathlib formalization of common math.

[Martin C. Martin]

Cool, I'll give that a shot!

[Kyle Miller]

You could also try something like Linear Algebra Done Right, which (I hope) is sufficiently abstract that you don't get bogged down in too many calculations.

[Martin C. Martin]

Of course, Lean already has the Filter stuff as a generalization of epsilon delta definitions. (I'm just thinking out loud at this point.)

[Kyle Miller]

Yes, and if you've done Patrick Massot's analysis tutorial, some of the main black box theorems you get to use are actually proved in Mathlib with all of that then given an epsilon-delta interface for the tutorial. (See this file)

[Martin C. Martin]

Cool, I have a copy of Linear Algebra Done Right, which I bought after seeing Baron Zweibach recommend it in his Quantum Mechanics class. I was looking for a reason to work through it. That could work well too!

[Martin C. Martin]

Thank you very much! This is certainly enough to chew on. I'm sure I'll be back with questions before long. :)

Is there a place to submit Lean-ification of classic textbooks like Spivak's or Axler's? Should there be?

[Kyle Miller]

Not yet! But if they're of good enough quality I think they could certainly live in the mathlib/archive folder

[Martin C. Martin]

Perhaps I'm getting ahead of myself. First I can do some formalizing, then we can worry about where to house it. :)

[Kyle Miller]

There's also another repository, the mathzoo that accepts more. The reason for being picky for mathlib is that every extra line of code is code that has to be maintained by the maintainers (and also all of mathlib has to pass continuous integration)

[Martin C. Martin]

Sure, I understand, and it makes perfect sense. Making something new and shiny is fun; maintenance is less fun, so can be harder for random contributors like me to keep up with. :)

[Yaël Dillies]

Should we start listing all such textbook formalisations somewhere? I know several people have worked on Linear Algebra Done Right in the past already.

[Kyle Miller]

I think there's no harm in having another, but yeah, it would be good to have an informal list of formalization projects

[Arien Malec]

Yaël Dillies said:

Should we start listing all such textbook formalisations somewhere? I know several people have worked on Linear Algebra Done Right in the past already.

yes please! Axler's coming out with an open content version soon -- would be fun to accompany that with corresponding proofs.