ErdosProblems/387: sync solved status

[williamjblair]

Summary
This updates Erdős 387 now that erdosproblems.com records the main question as solved negatively by Bui, Naprienko, Pratt, and Zaharescu.

The PR adds the BNPZ26 reference, changes erdos_387 to research solved with answer(False), and applies the same solved-negative status to the Guy c < 1 variant, which is also refuted by the result cited on the problem page.

Closes #4372.

Verification

• lake env lean FormalConjectures/ErdosProblems/387.lean
• lake build "FormalConjectures.ErdosProblems.«387»"
• lake --wfail build "FormalConjectures.ErdosProblems.«387»"
• lake --wfail build
• git diff --check

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