Tracking update of Erdos problem website (and Erdos 975)

Stream: Formal conjectures

[Seewoo Lee]

Hi, I'm now working on Erdos 975 (started few weeks ago but haven't pushed to repo yet), and the statement is slightly updated after me (and other person) made a comment on it. Originally it was for polynomials $f$ where $f(n) \ge 1$ for all $n$, and now it is for $f(n) \ge 1$ for sufficiently large $n$. Of course, this does not make any difference mathematically since we are only interested in the asymptotic (and actually this is quite annoying part for formalization). But I guess such update may happen for other problems without noticing it, and especially if the statement changes then one may also need to update formalization. Would there be a way to track it? I believe updates don't happen frequently though.

[Terence Tao]

The database at https://github.com/teorth/erdosproblems tracks the date of the last Lean formalization update, and the date of the last solution status update, but we don't have a mechanism for tracking when the erdosproblems.com formulation was last updated. Perhaps that can be a request one can place at https://www.erdosproblems.com/forum/thread/Site%20suggestions ? If every problem page comes with a "last modified" timestamp somewhere then it becomes possible to automatically flag when a problem has been modified after the formalization.

[Seewoo Lee]

Thank you! I'll put on suggestions then.

[Thomas Bloom]

I've added a 'last edited' sentence at the end of the problem description. This only appears if the problem has a timestamp, which isn't the case for most, since I only added the timestamp field a few days ago; but going forward it will reflect any edits made.

(Although this is edits to either the problem statement or commentary, so doesn't necessarily reflect a change in the actual problem statement that means the formalisation needs updating.)

[Seewoo Lee]

Thank you very much! I'll think about how can I integrate it as CI for the repository then.

[Thomas Bloom]

No problem - let me know if I can change anything on the website end to make it easier for you.

[Seewoo Lee]

I left it as an issue here with some vague ideas, since I may not have time to do it myself for now.