fix(ErdosProblems): 888

[danielchin]

Closes #4099

https://www.erdosproblems.com/888

• Changes the status of Erdos 888 to solved
• Add additional variants listed from the Erdos Problems website
• Add additional references
• Fix docstrings to display as LaTeX
• Format lines to be under the character limit

Assisted Gemini and Antigravity

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[mo271]

Thanks, LGTM!

[mo271]

Also needs updating the count in the Bench100 list... see failing build

[danielchin]

Updated the benchmark set count.