doc: before-requesting-review checklist (AGENTS.md + ErdosProblems README)

[williamjblair]

Puts the recurring review corrections into the two files authors and their agents already read:

• AGENTS.md: two rules that come up in review but weren't written anywhere: search FormalConjecturesForMathlib and neighboring files before defining anything (ErdosProblems: add 199, 224, 226, 246, 296, 363 (#3998 sync) #4343, ErdosProblems: add 31, 34, 47, 280 (#3998 sync) #4345), and keep notes-to-reviewers in the PR description rather than the Lean file (feat(ErdosProblems): add 755 #4036). Added to the existing Quality Checklist and DON'T list.
• FormalConjectures/ErdosProblems/README.md: a "Before requesting review" section with the Erdős-specific items (verbatim docstrings and solution attributions, ErdosProblems: formalise 11 solved problems, linking plby/lean-proofs #4319), following the pattern of the naming and docstring conventions already in that file.

Every line traces to a real review comment on a merged PR. Doc-only; follows up on the Zulip discussion about making the repetitive half of review a checklist authors and their agents tick off.

cc @mo271

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