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

[github-actions]

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

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

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