ErdosProblems: add 443, 484, 487, 497, 498, 502, 537, 582, 618, 646 (#3998 sync)

[williamjblair]

Adds Formal Conjectures statements for Erdős problems 443, 484, 487, 497, 498, 502, 537, 582, 618, 646.

Each statement follows the boxed problem text on erdosproblems.com (docstrings verbatim), cross-checked against the two hosted Lean proofs (plby and jayyhk). formal_proof links are pinned to a commit and included only where the hosted proof passed an axiom and hypothesis audit as unconditional.

Where a drafted statement departs from the hosted formalizations, the load-bearing choices:

• 443: parametrises the set as {k(m-k) : 1 ≤ k ≤ m/2} per the text; the hosted proofs use 1 ≤ r ≤ k-1, and the two images are equal by the symmetry k ↦ m-k. Carries n < m as in both hosted theorems, since at m = n the intersection is all of A n and the (mn)^{o(1)} bound is not intended.
• 484: states "at least cN" as c * N ≤ card over ℝ, verbatim from the text; the hosted proofs use the natural floor ⌊c·N⌋₊. Equivalent up to rescaling the existential c.
• 487: reads "positive density" literally as Set.HasPosDensity (the FC convention, cf. 741); both hosted proofs assume only lowerDensity A > 0, a weaker hypothesis, so the pinned proof covers this statement.
• 497: states the source's exponential form, antichain count = 2^{(1+o(1))·C(n, n/2)}; plby proves the equivalent log-side asymptotic. Counts via Nat.card of a subtype instead of a classical filter.
• 498: keeps the text's 1 ≤ ‖z_i‖ with the open unit disc. The closed-disc reading is false under that hypothesis (n = 1, z = 1: the closed disc at 0 contains both ±1), and Kleitman's proof is of the open-disc form.
• 502: the problem asks for the exact largest 2-distance set, which remains open between C(n+1, 2) and C(n+2, 2); what is solved (and machine-verified) is the Bannai–Bannai–Stanton upper bound, so the statement is |A| ≤ C(n+2, 2) rather than an IsGreatest form.
• 537: stated as answer(False) ↔ P with the text's ground set {1,…,N} (Finset.Icc 1 N, agreeing with jayyhk); plby uses Finset.range (N+1), which admits 0 ∈ A and trivializes the inner pattern. Both refutations go through the same Ruzsa counterexample.
• 582: requires G.CliqueFree 4 per the text ("contains no K₄", agreeing with jayyhk); plby proves the strictly stronger cliqueNum = 3, which implies this statement.
• 618: two readings shared with both hosted proofs and noted in the docstrings: "has diameter 2" is formalized as diameter at most 2 (the readings coincide for triangle-free graphs on three or more vertices), and the site's h(G) is read as the h₂(G) the problem itself defines.
• 646: reads "n! is divisible by an even power of each pᵢ" as "the exponent of pᵢ in n! is even", the reading of Berend's paper and both hosted proofs; the literal reading is trivially true at e = 0.

Happy to expand on any of these in review, including the hosted-vs-hosted disagreements.

Part of #3998.

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