Apply Bloom's statement-selection verdicts; add the bloom68 config

[tadamcz]

Applies Thomas Bloom's verdicts (emails of 2026-08-25/26) to the two Erdős datasets, and adds the canonical run config. With both bloom_selection subsets in effect, the benchmark totals 68 samples over 65 distinct problems: 50 in erdos (508 contributes three samples) + 18 in erdos_autoformalized (713 contributes two).

erdos (FC-formalized, 48 problems)

• 208 → erdos_208.parts.i: Bloom's explicit pick, overriding the earlier "stronger part" choice of parts.ii. (812 stays parts.i, already his pick.)
• 508 (Hadwiger–Nelson) resurrected as three samples: the value-typed HadwigerNelsonProblem stays an excluded manifest row, and three derived prove-or-disprove samples — χ(ℝ²) = 5, = 6, = 7 — stand in for it (Greg's proposal, adopted by Bloom). The derivation is a pure-text special case in scripts/erdos_isolation.py: the vendored Sources/508.lean stays byte-identical to the FC pin (the statement certificate is untouched), the target theorem is cut out, its answer(sorry) placeholder replaced by the literal, and the theorem renamed to HadwigerNelsonProblem.eqN — so each sample's id is its declaration name, per the usual convention. The fast suite re-derives the committed specs byte-for-byte; the container suite compiles them and certifies their .disproof declarations like every other spec (it skips only the answer-form certificate, which cannot apply to a value-typed source, and asserts the derived statement's type is sorryAx-free instead).
• bloom_selection is now 50 statements over 48 problems.
• ERDOS_PROBLEM_STATEMENT_SELECTION.md cut down to the selection rules plus Bloom's full list of 70 problem numbers; the per-problem table is redundant with subsets/bloom_selection.json.

erdos_autoformalized (18 problems, 20 statements)

• New subsets/bloom_selection.json, now apn_erdos_autoformalized's default subset: 18 statements — drops Erdos1206.erdos_1206.parts.ii (part i alone represents 1206) and Erdos1207.erdos_1207 (dropped from the benchmark entirely); 713 stays split into two samples. The manifest and vendored files are untouched.

configs/bloom68.yaml

The canonical eval-set config for the selection (the first git-tracked file in configs/): both tasks with their bloom_selection subsets, run with all affordances — agent_type: deep (subagents) and literature: true (offline arXiv snapshot) — per the 2026-08-28 agreement. gpt-5.6-sol + claude-fable-5, $200/sample cap (agreed; $27.2k hard ceiling), aligned with the recently launched configs (benchmarks@main, inspect-ai==0.3.259, retry_attempts: 5). Points at LeanOpenProblems@main, so launch after merge.

Notes for review

• Exactly one of χ(ℝ²)=5/6/7 is true, so two of the three 508 samples are disprovable-in-principle statements — worth keeping in mind when counting solve rates.
• The three derived specs have not been compiled locally (no local Lean toolchain); CI's isolation suite is the authoritative gate. χ(ℝ²) = 5 needs OfNat ℕ∞ 5, which Mathlib has, so this should be routine.
• Fast suites and mypy pass locally.