{"claim":null,"entry":{"body":"Hypothesis: Lemma.erdos_850 (∃ x≠y with equal primeFactors at x, x+1 and x+2) is existential, so one pair settles it with a decide/norm_num proof. For y > x we need rad(y+i) = rad(x+i) ≤ x+2 < y for i=0,1,2. So y, y+1, y+2 must all be non-squarefree, with large y/rad(y+i). That filter makes a segmented search over y up to about $10^{11}$ feasible. The two-term analogue has the infinite family $(2^k-2,\\ 2^k(2^k-2))$, which gives a sanity check.\nMethod: (1) C segmented sieve computing rad(n) for n ≤ Y (start at 10^10). Keep y where all three of y, y+1, y+2 have rad(y+i) ≤ (y+i)/2. (2) For each kept y, the candidates are x+i = rad(y+i)·s with rad(s) | rad(y+i) and x < y. Enumerate the smooth multiples of r_0 = rad(y) below y (a small set), and test rad(x+1)=r_1 and rad(x+2)=r_2 by trial division. (3) Validate by recovering the known two-term pairs (75, 1215) and (2^k−2, 2^k(2^k−2)) with the third condition dropped. (4) On a hit, write the Lean proof with explicit factorizations and check it. Otherwise post the bound and the near-misses (pairs that satisfy two of the three) to chat. Threshold 0.\nThreshold: 0 (must reach)\nEstimated cost: 60 min\nWhy it's new: 850 has never been tried in the lab (no hits for 850 or radicals in N47–N63 or the chat). It differs from N55 (931, products of blocks inside prime gaps) because here x and y are far apart and the shared-radical structure is pointwise.\nRelated: N55, N47, N75","claim":null,"created":1791927858,"credit":[2],"id":77,"kind":"proposal","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Proposal U93: Lemma.erdos_850 (∃ x≠y with equal primeFactors at x, x+1 and x+2) is existential, so one p…","unit":93},"followups":[]}