Issue for already formalized problems

Stream: Formal conjectures

[Franz Huschenbeth]

There are some problems, which have been formalized but dont have a corresponding issue.

Should we open a issue (and close it with reference to the corresponding PR), if the problem is part of some list that we track via milestone? There are about 100 such problems for the Erdös Open Problems Milestone.

[Franz Huschenbeth]

Similarly how should we handle problems which are too vague (see https://www.erdosproblems.com/1163), but are from a certain list. Should we create a issue and close it with a message that the problem is too vague or just leave it out. Or maybe document it in the milestone description or somewhere else...

[Moritz Firsching]

For the second question: I'd say keeping the issue vague questions open, perhaps there will be at least some variants that show progress. Also Hilbert's problem list has such questions.
It is easy to make problems a little imprecise, for instance https://epoch.ai/frontiermath/open-problems/apery-irrationality "prove the irrationality of other “famous” constants", whithout a precise definitions of "famous".

[Moritz Firsching]

Regarding opening issues for the one that never had an issue on github:
For the one that do have a pull request it is easy: just add the milstone to the pr instead of the issue.
There is probably still quite some left that have neither a pull request nor an issue, because they were already part of the initial version of the repo.
I suppose no harm would be done by opening and then immediately closing the milestone (perhaps best with a link to the corresponding file to make sure no errors are made).
That would make the percentage count on the Milestone accurate!

[Franz Huschenbeth]

Moritz Firsching said:

Regarding opening issues for the one that never had an issue on github:
For the one that do have a pull request it is easy: just add the milstone to the pr instead of the issue.
There is probably still quite some left that have neither a pull request nor an issue, because they were already part of the initial version of the repo.
I suppose no harm would be done by opening and then immediately closing the milestone (perhaps best with a link to the corresponding file to make sure no errors are made).
That would make the percentage count on the Milestone accurate!

What is with cases like this https://github.com/google-deepmind/formal-conjectures/issues/1937#issuecomment-3823673035. Wouldnt it make more sense to just have one tracking issue for every problem, instead of it being scattered over issues and PRs.

I have just gone ahead and created issues for all problems, which are in the repo but not in the milestone because finding the PR takes pretty much the same time + arguments above.

[Moritz Firsching]

I think there are very few prs in the milestone currently. I tried searching for them but https://github.com/google-deepmind/formal-conjectures/pulls?q=is%3Apr+milestone%3A%22All+open+Erd%C5%91s+problems+formalized%22+ returns nothing for some reason, but there should be maybe two or three like this?

[Moritz Firsching]

I suppose it then makes sense to also create issues for those last few!

Thanks for doing all that!

[Franz Huschenbeth]

Moritz Firsching said:

I think there are very few prs in the milestone currently. I tried searching for them but https://github.com/google-deepmind/formal-conjectures/pulls?q=is%3Apr+milestone%3A%22All+open+Erd%C5%91s+problems+formalized%22+ returns nothing for some reason, but there should be maybe two or three like this?

Oh yeah sorry, there were 5, 2 of which had issues which were also in the milestone and 3 had none for which I created a issue. So I removed them all and opened the corresponding issues when needed.