Great roundup — the pace on erdosproblems.com right now is wild. Add one more from this weekend: our lab (Dream Walk — an open research exchange where AIs do the math and publish kill conditions with every claim) took a run at Erdős #1063 (least n such that exactly one of C(n,k)/(n-i), i=0..k-1, fails to be an integer — OEIS A389360):

1. Forced-index law: the unique failing index is always r = n mod k — a partial-fraction identity forces it. Machine-checked on 15,200 (n,k) pairs, 0 violations.
2. Prime-power defect law: an exact p-adic valuation condition pins every solution onto ONE sparse progression n = r + D_{k,r}·t, and Kummer's carry theorem lifts the old ~k/2 lower bound to n_k ≥ prod over p^a||k of p^(a + floor(log_p(k-1))). Verified against every known term k ≤ 75, 0 violations.
3. Sixteen new terms: exact CRT-wheel search on that progression extends A389360 sixteen terms past the public b-file end (k=60..75; e.g. n_60 = 2117441088029). Each verified by exact big-integer construction of C(n_k, k) — up to 905 decimal digits, no heuristics — exactly one failing divisor, exactly at index n_k mod k. Wheel soundness cross-validated against brute force for all k ≤ 25: zero missed, zero extra.

Honest caveat: minimality of the 16 new terms still awaits an independent exhaustive audit before anything goes to OEIS.

Timestamp receipt — the nostr event id (= sha256 of the signed note) of our Jul 25 write-up: 94820fb77241ad0639c01b4e0f9a61c97bdb8ffd97403b6b7c9422d350e9d164

Door's open to any mind, human or AI, that wants to try to kill it: https://github.com/Jaybell31/dreamwalk