Erdős Problem 125: status mismatch (repo=formally solved, erdosproblems.com=open)

[github-actions]

The status of [Erdős problem 125]appears to have changed.

• This repo: formally solved (in FormalConjectures/ErdosProblems/125.lean)
• erdosproblems.com/125: open

Please verify and update the @[category research ...] annotation if appropriate.

[mo271]

needs fixing on the erdosproblems side...

Although it is not quite clear if the upper density will also be added as part of the main variants