TODO lists

Stream: mathlib4

[Snir Broshi]

I have a big list of stuff that's missing from Mathlib, and I assume others have similar lists.
I think merging all of those lists would be beneficial, and would let us see at a glance what's missing and who's working on it, and also what's missing from the list of what's missing.

I then thought about opening a Trello board or a self-hosted Wekan, then I thought about GitHub issues & projects.

Ruben Van de Velde said:

Snir Broshi said:

Is there somewhere else the TODO to implement it could live?

An issue on the mathlib repository? (I think we should use that more)

What's your opinion on opening lots and lots of issues? This could be things like small theorems or definitions (e.g. Definition: Edge covers for simple graphs), but also the 981 remaining items from Freek's 1000+ list and the 346 remaining IMO problems.

I think having a dedicated place to collect discussions for each of these is worthwhile, if only to link to previous Zulip discussions so that they don't get forgotten.

To keep the issues organized we can use labels and GitHub's projects feature.

This is more issues than Mathlib ever had, including mathlib3. If such "issue spam" is problematic, then I'll open a Trello/Wekan.

[Bryan Wang]

I suggested something vaguely similar a while back (#mathlib4 > What is not yet in mathlib?) and would be rather happy to see this happen!

[Ruben Van de Velde]

I'd be in favour, but only if there's something useful you can say. For example, I wouldn't open an issue with nothing more than "Theorem X from 1000.yaml is missing"

[Ruben Van de Velde]

If you can state the theorem and link to x, y, z definitions or theorems that are relevant, or issues #a #b #c to add those results, that would make more sense. Or an issue like "missing theorems from 100.yaml about Euclidean geometry" with a checklist might be useful to spot dependencies they have is common

[Snir Broshi]

The problem I see is that because there's no such "nothing" issue, people don't share info about it.
We need empty organized places to collect discussions.

[Snir Broshi]

A monolithic issue would half work, it requires copying every comment made on it to the appropriate location in the huge issue description.
Alternatively, that issue could say something like: "prefix every comment you make here with the list number [ITEM 123] to make it easily searchable"

[Snir Broshi]

Ooh dependencies is a good one, GitHub recently added support for creating dependencies between issues, even across repos
image.png

(example from the vscode repo https://github.com/microsoft/vscode/issues/251621)

[J. J. Issai (project started by GRP)]

As a trial balloon, I would suggest a small collection organized by topic (or by Mathlib folder), where a missing item is associated with the topic or folder to which it should belong. Also, rather than populate this collection with all the desired items, prioritize from each list (and for each topic/folder) the top two or three (or ten) items, and then add a link to a longer list of items.

This presents the missing items in a small not overwhelming batch. Further, if an item links to one or more topics/folders, one has a chance at seeing this and suggesting an appropriate generalization (or referring to an existing one in Mathlib, in which case the work is autoformalized specialization). Arranging it by topics allows one to find the missing item of interest more quickly. Keeping the lists short allows for efficient (if slow and gradual) merging from other longer lists.

In updating this list, one can move a "found" item off this list and onto a different list to help measure the success of this structure. One can also quickly estimate the constant in Kevin Buzzard's O(1000) needed definitions for current mathematical development.

[Kevin Buzzard]

It is not immediately clear to me that telling the world "346 IMO problems are missing from Mathlib" is helpful. The point of the IMO formalizations in mathlib is that they are supposed to be "model answers" demonstrating that our library is up to making slick solutions; I fear that just flagging that we seem to accept IMO problems and have hundreds missing might just open the door for people to use AI to write crappy solutions; what we actually want is far more nuanced.

This question of how to list stuff which is missing from mathlib has of course come up before, and one reason that there is no definitive answer is perhaps because different people have different opinions about whether something is "missing" or "unwanted".

[J. J. Issai (project started by GRP)]

As a further recommendation, a tag of (easy/medium/hard) could be added to help spur community action to add certain missing items.

[Snir Broshi]

Kevin Buzzard said:

I fear that just flagging that we seem to accept IMO problems and have hundreds missing might just open the door for people to use AI to write crappy solutions; what we actually want is far more nuanced.

Then perhaps a separate GitHub repo just for issues or a Wekan will be enough to hide such a list from the AI slop people? Avoiding slop is a hard problem, but I don't think we should sacrifice TODO lists to avoid slop.

[Ruben Van de Velde]

No, the point is that "solutions to imo problems" is not something the mathlib community considers a "todo"

[Snir Broshi]

Okay then let's exclude IMO from the discussion

[Kevin Buzzard]

That's definitely a step in the right direction. The next question is: what gives you the authority to claim that something is missing (and hence, implicitly, desired)? And what happens when someone finds your list, spends days making a PR adding something, and then the maintainers say "actually no we don't want this" and they say "but I read on this list that you did"?

[Kevin Buzzard]

Even the maintainers cannot write a coherent list of what is desired in mathlib (because they have conflicting views on the question).

[Snir Broshi]

That's a good question, and the answer is I don't have any authority, but I do think non-authoritative suggestions for what's missing are valuable.

[Kevin Buzzard]

ok well my list is here #general > O(1000) definitions for Annals @ 💬 . And I am not speaking for the maintainers when I say "I think we want these", I am speaking for myself.

[Snir Broshi]

The problem that you describe can already happen even without issues, e.g. #33921 started by fixing a TODO left in the code by a maintainer after getting support from multiple maintainers, and then it was decided that this TODO was actually a mistake and Mathlib doesn't want to fix it.

[Kevin Buzzard]

I absolutely agree that this is a complex problem and also that people's opinions change and that sometimes things are not updated when opinions change.

[Snir Broshi]

And yes it wasn't great getting an "actually no we don't want this" response, but it wasn't horrible, and I think it would happen less with GitHub issues vs TODOs sprinkled in the code

[Bryan Wang]

My idea back then was that the 'definitive' list can only be updated by a PR to mathlib, just like Missing undergraduate mathematics in mathlib. But I appreciate that this is more complex than it would seem at first glance.

[Snir Broshi]

Issues aren't meant to be a definitive list, just suggestions from random contributors, much like the RFC issues in core. If the maintainers don't like an issue they can close it at any point.

[Snir Broshi]

Basically what I'm saying is: I want to make my TODO list public and let people modify it and claim things off of it. Do others want that too?

[Kevin Buzzard]

You are also saying "I might want to open possibly hundreds of issues against the mathlib repo" which might get a less positive reception than "I want to create a text file which probably most people will never find". I do not know what visions the maintainers have for the issues; personally I don't look at them because I am able to generate my own issues so am less focussed on trying to solve other people's issues :-/

[Snir Broshi]

Yeah that's why I'm asking for feedback before spamming issues.
(btw "text file" is not what I had in mind)

[Snir Broshi]

Here are examples where an unofficial list of things to do in graph theory would have been helpful:
#new members > Looking for a first project (Graph Theory / Combinatorics) @ 💬
#graph theory > Newbie lurker here, trying to restart @ 💬
#new members > Menger's theorem @ 💬
#new members > edge connectivity @ 💬
And by unofficial list I mean a list maintained by all graph theory contributors.

[Snir Broshi]

J. J. Issai (project started by GRP) said:

As a trial balloon, I would suggest a small collection organized by topic (or by Mathlib folder), where a missing item is associated with the topic or folder to which it should belong. Also, rather than populate this collection with all the desired items, prioritize from each list (and for each topic/folder) the top two or three (or ten) items, and then add a link to a longer list of items.

Here's my attempt https://github.com/leanprover-community/mathlib4/issues?q=is%3Aissue%20state%3Aopen%20author%3ASnirBroshi

[Bolton Bailey]

I try to solve the problem of having my ideas publicly accessible without spamming the main repo by opening issues on my fork instead, I don't know if that would meet Snir's goals, but perhaps it's an option to consider.

[Yaël Dillies]

Here are my thoughts:

1. Open one issue per problem, not one issue per list. This way, the issue is more focused and stands a chance of being closed.
2. Only open issues for which there is relevant past discussion to summarise.
3. When opening an issue, summarise past discussions, link to them and make sure to clarify what qualities are expected for a contribution to close the issue

[Yaël Dillies]

If you follow these three points, then I expect these issues to act as a useful way to access the community's opinion on some matter!

[Edward van de Meent]

i think the goal here is not necessarily to ask the community opinion, but just to have a heap/collection of concepts which could reasonably be PRed to mathlib. keeping track of which ones have prior discussion, which ones have been (a priori) blessed/rejected by maintainers, etc. is also important, but having the overview of what isn't but could be is what i understand to be the main point here.

(let me emphasise that keeping track of rejected topics is useful, as i don't believe this has been mentioned yet)

[Yaël Dillies]

Sure, but I claim that a rejected topic should be tracked by a closed issue

[Violeta Hernández]

Kevin Buzzard said:

It is not immediately clear to me that telling the world "346 IMO problems are missing from Mathlib" is helpful. The point of the IMO formalizations in mathlib is that they are supposed to be "model answers" demonstrating that our library is up to making slick solutions; I fear that just flagging that we seem to accept IMO problems and have hundreds missing might just open the door for people to use AI to write crappy solutions; what we actually want is far more nuanced.

Back when we started writing IMO problems for Mathlib, the infrastructure for creating other projects was far less established. I wonder what we'd lose if we simply told people to contribute on compfiles instead.

[Yury G. Kudryashov]

I agree that IMO is a natural candidate for a child-of-Mathlib project. We should encourage people to PR supporting lemmas though, or close API gaps they found while working on IMO problems.

[Joseph Myers]

The main thing we lose from contributing directly to compfiles is exactly the review process that looks for lemmas that could be extracted to mathlib in appropriately general form and expects them to get through review and be merged before the IMO PR can go in. (The most interesting IMO PRs are those that do lead to such lemmas being added, not the subset of problems, especially algebra and number theory, that don't show up missing lemmas.)

Also, do cross-repository PR dependencies work so that a compfiles PR could be opened with dependencies on 25 mathlib PRs to illustrate the goal those mathlib PRs are working towards? That would have the added complication of needing to depend on a mathlib branch with the 25 PRs integrated.