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

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

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

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

Start by reading FormalConjectures/ErdosProblems/1188.lean and comparing its @[category research ...] annotation with the current status on erdosproblems.com/1188. Verify which status is correct, update the annotation if needed, and confirm the file remains consistent with the external problem record.

Written by the indexing model from the issue text.