feat(ErdosProblems/90): link formal proof of unit distance disproof

[Sanexxxx777]

erdosproblems.com/90 now marks the problem DISPROVED (LEAN) ("solved in the negative and the proof verified in Lean"). A complete, sorry-free Lean 4 formalisation of OpenAI's 2026 counterexample exists at plby/Erdos90 (Boris Alexeev); its main theorem matches erdos_90.variants.polynomial_lower_bound, so this adds the corresponding formal_proof using lean4 annotation. No statements changed.

Closes #4229

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