TASK: attempt open problems from the Justin Sun Prize bank (github.com/TheJustinSunPrize/awards, problems/). Work on ONE problem per agent.

Problems (JSP id — catalog paraphrase):

1. JSP-000246 — Can separated integer intervals be chosen so that the reciprocals of all their integers sum to one?
2. JSP-000294 — Can distinct-element sums from the union of two floored exponential sequences represent every sufficiently large integer?
3. JSP-000340 — Are there infinitely many n such that m + ω(m) ≤ n for all m < n? Same with c·ω(m) for any fixed c > 0?
4. JSP-000372 — Is lcm(1..p_{k+1}−1) always smaller than p_k · lcm(1..p_k)?
5. JSP-000550 — Must two disjoint equal-length intervals of consecutive integers have different lcm?
6. JSP-000617 — Can an integer set have uniformly bounded two-term representation counts while its sumset density is arbitrarily close to 1?
7. JSP-000682 — Is there an integer n such that d(n+k) is bounded linearly in k for all k?
8. JSP-000738 — Is there a uniform constant bound on the number of divisors of n in an interval of length n^{1/4} near √n?
9. JSP-000773 — Which disjoint intervals of consecutive integers have products with exactly the same set of prime factors?
10. JSP-000947 — Is there an integer n such that n − 2^k is prime for every permitted 2^k < n?
11. JSP-000951 — Does adding the set {2^a·3^b} always strictly increase the Schnirelmann density of another integer set?
12. JSP-001004 — Does every 2-coloring of ℕ contain an infinite set whose specified pairwise sums all have one color?

STEP 0 (mandatory, before any math):

• Find the exact original statement: the problem's page on erdosproblems.com or the original Erdős paper. The catalog text is only a paraphrase.
• Check current status on erdosproblems.com, arXiv, and the open PRs/issues of the repo. If it is solved, or someone has an active complete-solution claim, STOP and report "taken".

STEP 1: try to solve the original statement completely (proof, disproof, or counterexample). Partial progress is not eligible, so do not claim it as a solution.

STEP 2: if solved, write a Lean 4 + Mathlib formalization of the EXACT original statement, compiling with no sorry and no extra axioms (check with #print axioms).

RULES:

• Never claim a solution without a compiling Lean proof.
• Do not post anything publicly, do not open PRs, do not submit claims.
• Report back only: JSP id, exact statement + source link, status check result, outcome (solved / counterexample / no result), the proof sketch, and the Lean file. If no result, say so in one line.