The status of [Erdős problem 397](https://www.erdosproblems.com/397) appears to have changed. - **This repo**: `solved` (in `FormalConjectures/ErdosProblems/397.lean`) - **erdosproblems.com**: `formally solved` Please verify and update the `@[category research ...]` annotation if appropriate.