ErdosProblems: add 24, 93, 164, 314, 315, 333, 369, 401, 429, 435 (#3998 sync)

[williamjblair]

Adds Formal Conjectures statements for Erdős problems 24, 93, 164, 314, 315, 333, 369, 401, 429, 435.

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:

• 24: uses Mathlib's SimpleGraph.copyCount G (cycleGraph 5) for the C₅ count; the hosted proofs count labelled embeddings divided by 10. The two counts agree on every graph.
• 93: stated in FC's concrete ℝ² (house style of the sibling problems 982 and 1082); the hosted proofs quantify over an abstract two-dimensional inner-product space. Equivalent up to isometry.
• 164: keeps the text's primitivity definition verbatim and adds ∀ a ∈ A, 2 ≤ a as a separate hypothesis. The floor does real work here: without it, Lean's junk value 1 / (1 * Real.log 1) = 0 would let A = {1} satisfy the bound even though the informal summand is undefined there.
• 314: wraps the liminf equality in FC's answer(True) ↔. jayyhk states the bare equality; plby proves a block-existence form that implies it via minimality. The draft follows the text's ε(n) formulation.
• 315: the text says a₁ < a₂ < ⋯, so the draft uses StrictMono. This matches jayyhk and departs from plby, which assumes only Monotone; the two hosted proofs disagree with each other here, and the draft follows the text.
• 333: stated as answer(False) ↔ P per FC style for a disproved yes/no question (cf. 263.parts.ii); jayyhk proves ¬P directly and plby stops at the counterexample pair.
• 369: the text as literally written is trivially true, as the site commentary itself notes. The draft formalizes the commentary's non-trivial variant, with the k consecutive integers confined to [n/2, n]; that variant is what the "proved (Lean)" status refers to and what both hosted proofs establish. The docstring records this.
• 401: follows the text and jayyhk's shape, ∃ f → ∞, ∀ r ≥ 1, …; plby proves the property for one explicit witness ω(r) without the existential wrapper.
• 429: states the question positively as answer(False) ↔ P; both hosted proofs state the refuting construction, which is the negation of P. "Sparse enough" becomes a counting-function threshold with f → ∞, and the Tendsto condition does real work: with f = 0 the hypothesis class would degenerate.
• 435: renders "the largest integer not of the form …" as IsGreatest; the hosted proofs state membership plus an upper bound, which is equivalent. The two hosted final theorems are byte-identical on this problem.

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

Part of #3998. Fixes #493, fixes #697, fixes #712.

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

[mo271]

please mark as "Ready for review" when ready for review

[williamjblair]

@mo271 good for review now!