Resolves YES if by july 2027 an LLM-based system produces a set of positive integers with divergent reciprocal sum but no arbitrarily long arithmetic progressions, with the proof either formally verified or accepted by expert consensus. The LLM must be credited with the core construction/proof. If it's ambiguous who gets credit between LLMs and AIs, I'll resolve based on the majority opinion among human mathematicians. Non-constructive disproofs of the Erdős conjecture don't count; the set must be exhibited.