Open Erdös Problems Milestone: Which Status count as open

Stream: Formal conjectures

[Franz Huschenbeth]

I am assuming that we take https://github.com/teorth/erdosproblems/blob/main/data/problems.yaml as ground truth for the milestone.

The problem is that there are several status, which count as open, while the status is not exactly open. This includes "decidable", "verifiable", "falsifiable", "independent", "not provable", "not disprovable". All other open problems have status "open".

There is also the classification between 'solved' and 'open' on the Erdos Problems Website, which colors problems as green (solved) and red (open). Based on the coloring the status "open", "verifiable" and "falsifiable" count as open (red) and all other status from above count as solved (green).

I would thereby propose that the milestone just tracks all problems of the Problems YAML, which have status "open", "verifiable" or "falsifiable".

[Franz Huschenbeth]

@Moritz Firsching Can you add that / clarify that in the milestone description? The number of open problems (of these 3 statuses) are currently 685 then.

[Franz Huschenbeth]

https://www.erdosproblems.com/580 Ok, this problem is decidable but colored red (open), might be because the computation to decide it is galactic and so it is not really solved (we just know it can be proven or disproven and is not independent :D).

So we could in general include the decidable problems or exclude them in our open problems (they are like 8 of them). I think both pretty much works. Having a formalization more than less does not hurt though.

[Moritz Firsching]

I'd add "decidable" to the unsolved category

[Franz Huschenbeth]

Ok will add the 8 "decidable" problems to the milestone then.

[Ralf Stephan]

Highly recommended reading:

https://arxiv.org/abs/2601.22401

[Yaël Dillies]

This is a lot of words to say "Thomas Bloom doesn't know every single relevant article that has ever been published"

[Franz Huschenbeth]

This probably also part of the reason why Terence Tao created the erdos problems wiki repo as a crowdsourced project to better track the different statuses of the erdos problems.

Or is the erdos problems wiki the ground truth for the erdos problems website anyway? I am not entirely sure.

[Thomas Bloom]

The status is taken directly from the wiki these days (so others can update it), but the green/red setting is manually by me. Usually these agree anyway, since I or others update the wiki at around the same time as I change the site when a solution is given/discovered.

[Thomas Bloom]

(deleted)

[Thomas Bloom]

The status on the wiki is only ever a summary (sometimes somewhat arbitrary) of the qualitative description of the results given on the website.

[Thomas Bloom]

E.g. it is somewhat of a matter of taste for a lot of problems when they count as 'solved', like when something is proved for all large integers and what remains is (in principle) a finite computation

[Alex Kontorovich]

Now that the Erdos 392 formalization is done (in PNT+), I wonder if it makes sense to link the formal statement to the solution? If so, what's the simplest way to do so?

[Yaël Dillies]

Please do so, that would be great! As of last week, FC has a new variant of the @[category] attribute. You can do category research formally solved at <link>

[Moritz Firsching]

See also https://github.com/google-deepmind/formal-conjectures/issues/2381

[Paul Lezeau]

Done in FC#2389