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

The status of [Erdős problem 521](https://www.erdosproblems.com/521) appears to have changed.

- **[This repo](http://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/521.lean)**: `formally solved` (in `FormalConjectures/ErdosProblems/521.lean`)
- **[erdosproblems.com/521](https://www.erdosproblems.com/521)**: `open`

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

Start by comparing FormalConjectures/ErdosProblems/521.lean with the linked erdosproblems.com/521 entry, focusing on the @[category research ...] annotation. Verify the current status from the available references, then update the annotation if the repository is incorrect. Done means the repository status agrees with the verified problem status.

Written by the indexing model from the issue text.