feat(ErdosProblems/888): record 2026 order-of-growth solution

[Sanexxxx777]

erdosproblems.com/888 now marks the problem SOLVED: the order of growth of the extremal set is $\Theta(n \log\log n / \log n)$ — the semiprimes (noted by Cambie and Weisenberg) give the sharp lower bound, and a matching upper bound $f(n) \ll n \log\log n/\log n$ was proved by GPT-5.5 Pro (prompted by Chojecki). This records both sharp bounds as research solved variants and updates the module docstring.

The main theorem erdos_888 asks for the exact value of Nat.findGreatest, which is only known up to constants, so it stays research open — happy to adjust if the maintainers prefer a different treatment.

Closes #4099

[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.

[danielchin]

Looks like I may have beaten you to the punch, this is a duplicate of #4376

[Sanexxxx777]

You're right — #4376 covers this and more (the status change matches the site's SOLVED marker, plus the category-count fix in FC100OpenSet1). Closing in favour of yours. Thanks for pointing it out!