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

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

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

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

Open FormalConjectures/ErdosProblems/489.lean and compare its @[category research ...] annotation with the current status at erdosproblems.com/489. Verify the status discrepancy, update the annotation if appropriate, and run the repository’s validation for the file. Done means the repository annotation matches the verified problem status.

Written by the indexing model from the issue text.