Status of mathlib

Stream: general

[Jagadish Bapanapally]

I am new to Lean. I want to formalize Fast Fourier Transform in Lean which is not formalized yet as per the info in this link: https://leanprover-community.github.io/undergrad_todo.html. So, is it ok for me to work on it? Is there any way to find out what's currently being formalized in Lean?

[Eric Wieser]

A good way to work out if someone else is already working on something is to:

• Search this Zulip
• Search the GitHub PRs (open and closed)
• Ask on Zulip as you just did!

[Patrick Stevens]

A question from the peanut gallery: if current trends continue, the port of mathlib from Lean 3 to Lean 4 will be nearly done in a few months. Would people recommend starting a new project like this with Lean 3 (with access to all of mathlib, but in a few months when mathlib[3] stops accepting PRs you have to learn a slightly different language and use mostly-automated-tooling to port your work in progress to mathlib4), or with Lean 4 (where you have access to only the most foundational 60% of mathlib right now)?

[Eric Wieser]

I would recommend doing this in lean3 simply due to mathlib access; but if you're a new lean user, it is probably better to do this in a standalone project rather than PR it to mathlib

[Eric Wieser]

I expect the "mostly-automated-tooling" story to be much better at standalone projects than at PRs.

[Scott Morrison]

I think the answer depends a bit on what the subject area of the project is.

[Scott Morrison]

But I would say the opposite: if at all plausible, just work in Lean 4.

[Bolton Bailey]

Question: Is mathlib4 currently accepting PRs not related to the port? Even if they aren't being focused on now, is it ok to make PRs and just expect them to be backlogged for a few months?

[Scott Morrison]

If they are solely new files, based on completely ported files, yes please, PRs accepted!

[Scott Morrison]

If they add new lemmas that need to go in earlier files, those are fine too, we'll just need to think a little about how to label them / whether to just put them in the right place already.

[Scott Morrison]

We have been discussing marking some files which are ported and have all downstream dependencies ported as "archived", which can be freely modified in mathlib4 without needing backporting. The framework for that is not quite settled!

[Kevin Buzzard]

I have two students in London working on dimension theory in lean 4 and I encouraged them to PR to mathlib 4: their work will live in new files and won't be backported

[Matthew Ballard]

My graduate class this past semester started in Lean 3 and ended up in Lean 4 :lol: They wanted to do some things with edge colorings of graphs and all the dependencies had been ported. With decreasing depth in the unported dependency graph, we are getting close to “port the things I might need if not ported” being reasonable advice.

[Yaël Dillies]

What were the edge coloring results? @Bhavik Mehta just proved a bunch of those.