Vela

Is it true that for every there exists some prime such that

Open problem — our best result is machine-sealed: verified reduction, reproduced by an independent verifier. The conjecture itself is unsettled.

number theory · open · formalized (Lean) · 11 attempts

machinery: Kummer-carries,g_kr-divisors,consecutive-integer-window,prime-distribution,Baker-Wustholz-linear-forms,abc/kernel-bound,effective-finiteness,exhaustive-search-certificate,binomial-valuation

use this record

vela registry pull vfr_37aec80d874a0239
vela reproduce examples/erdos-problems

routes

verified computationpython:verify_699_central_doubling.py

central-doubling exact reduction re-check (pinned tier: scripts/requirements-verifiers.txt)

formal prooflean

Lean patch building clean under the math CI profile (no sorry, no new axioms)

obstruction reportreview

precise, artifact-backed reason a route cannot work

banked

the central-doubling reduction + CRT obstruction verified; the two arms provably do not meet

targets

the gap between the arms is the open obstruction.1

evidence

honest null

needs verification

Candidate sweep (#699,#287,#993,#1082): all DISQUALIFIED as maps-not-closes; #488 the lone sliver (|A|=2 partial). Each has a cheap verifier but the open direction is a universal whose close is an analytic/incidence/structural wall.

Workflow erdos-candidate-assessment (wf_617a7e8e). #699 (binomial-gcd Sylvester-Schur, Lean-formalized): p>=i statement true to n=400, exact exceptional set for p>i recovered incl gcd(C(28,5),C(28,14))=1080; close = Kummer/Legendre valuation NT wall. #287 (Egyptian-1 consecutive-gap>=3): true to M=24 (witness [2,3,6]); proof route = Sophie-Germain/(p+1)/2 prime density, Hardy-Littlewood wall. #993 (tree independent-set unimodality): true to n=9; log-concavity breaks at n=26 (Kadrawi-Levit), unimodality never; structural-combinatorics wall, enumeration-evidence trap. #1082 (no-3-collinear distinct distances): Part II (single-point n/2) already FALSE (Harborth 1996); Part I (total n/2) is a lower-bound conjecture, Guth-Katz incidence wall; framing conflated the closed and open halves. PATTERN CONFIRMED: cheap verifier alone does NOT predict a close; the deciding factor is whether the open direction has a finite witness/movable extremal quantity (none here). Useful byproduct: van Doorn 9/10 (#302) and 25/28 (#301) baselines re-confirmed from the live page via curl.

verified reduction

machine-sealed

#699 (OPEN): GPT-Pro reduction VERIFIED correct -- Kummer/Lucas form (p|gcd(C(n,i),C(n,j)) iff i and j both NOT digit-dominated by n in base p), proves i=1,2 + fixed-(i,j) large-n, and reduces ALL to the THRESHOLD LEMMA. But this is exactly the lemma a submitted proof (Parthasarathy 2026) attempted and Bloom DECLARED INVALID -- so the crux is hard, not a quick win.

GPT-Pro structural attack (Opus-verified). Kummer: p|C(n,k) iff k not <=_p n (digit domination). #699 bad-condition: forall p>=i, i<=_p n OR j<=_p n. Case A (p>j): witness iff P+(n(n-1)...(n-i+1))>j, so counterexample needs last i factors j-smooth. Rough-part obstruction (sec6): R_{>=i}(C(n,i)) | C(j,i), PROVING i=1 (would need n|j) and i=2 (would need C(n,2)|C(j,2), impossible j<n). Sec7: fixed (i,j) holds for all large n (sublinear j << n^{1-pi_{<i}/i}), NO prime-distribution input. THRESHOLD LEMMA (the crux): if no prime p>i divides both C(n,i),C(n,j) then i is prime and i|both => done. OPUS INDEPENDENT VERIFICATION (digit-domination, n<=400, all 1<=i<j<=n/2): official exists-p>=i has ZERO failures; FO triples (where stronger exists-p>i FAILS) are EXACTLY {(10,3,5),(16,2,6),(28,3,14),(28,5,14),(244,3,122)} = Cong's list in range; ALL FO triples have i PRIME and saved by p=i exactly -> Threshold Lemma holds with 0 violations. Matches Cong's Rust to n=1e7 + 2^k to 1.34e8 + 3^m+1 to 1.29e8 (i=2 at powers of 2, i=3 at 3^m+1 with j=n/2, i>=4 only (28,5,14)). CRITICAL CONTEXT (erdosproblems.com/699 comments): #699 is OPEN. Parthasarathy (2026) 'An Effective Proof...' (J.Exp.Math, under review) claimed full resolution with the SAME tools (FO Characterisation, Carry Lemma ~ GPT's Threshold Lemma) + Lean (27 thms, 0 sorry) -- but Thomas BLOOM reviewed it and declared it INVALID ('not formalising anything like the statement'). StijnC flagged a specific Case-B hole (i<q<j where C(n,j),C(n-i,j-i) not multiples of q while C(j,i),C(n,i) are). So GPT independently re-derived the natural reduction, but the remaining Threshold Lemma is exactly where a serious attempt FAILED -- treat as hard/analytic-risk, verify ruthlessly, do NOT overclaim. VELA OPPORTUNITY: not to claim the lemma (Parthasarathy trap) but (a) the verified structural map + correct Lean of what is ACTUALLY proven (i=1,2 + threshold reduction + FO verification), and (b) any Threshold Lemma attempt must be adversarially tested against StijnC's Case-B shape. The Parthasarathy 'Lean proof that does not formalise the statement' is itself a textbook Canopus trust-layer case.

claimcomputational_search · proposer:GPT-Pro (attack) + Opus 4.8 (v — GPT-Pro (attack) + Opus 4.8 (vcomputational_search · proposer:GPT…GPT-Pro (attack) + Opus 4.8 (vexact_arithmetic_recompute · opus:independent(PuLP-CBC/exact) — Opus 4.8exact_arithmetic_recompute · opus:i…Opus 4.8

verified reduction

machine-sealed

#699 PROGRESS (GPT-Pro, Opus-verified): the Bloom/StijnC hole is FIXED. GPT proved a SHIFT LEMMA (p>i, p∤C(n,j) => v_p(C(n,i)) <= v_p(C(n-j,i))) that survives Case B, giving the corrected reduction: if no prime p>=i divides both C(n,i),C(n,j), then R_{>=i}(C(n,i)) | C(n-j,i). The Threshold Lemma now reduces to a clean ROUGH-GROWTH LEMMA: R_{>=i}(C(n,i)) does NOT divide C(n-j,i) for all 1<=i<j<=n/2. Verified true to n=260 (FO witnesses always p=i). STILL OPEN: the Rough-Growth Lemma is unproven (the new, cleaner crux).

GPT-Pro corrected its earlier attack. OLD rough-part step used C(j,i) and the FALSE move 'p|A,p∤B => p|E=C(n-i,j-i)' -- exactly what StijnC's Case B refutes and Bloom rejected. FIX: replace C(j,i) by the SHIFT C(n-j,i). SHIFT LEMMA (proven, Opus-verified 0 violations to n=260): for p>i prime with p∤C(n,j): v_p(C(n,i)) <= v_p(C(n-j,i)). Proof (Kummer): v_p(C(x,i))=#{a>=1: x mod p^a < i} for p>i; if n mod p^a=alpha<i<p then digit-domination j<=_p n forces j mod p^a=beta<=alpha<i, so (n-j) mod p^a=alpha-beta<i, counting the same a. Survives Case B because it asserts only v_p(D)>=v_p(A) (from BD=AE), never p|E. CORRECTED REDUCTION: Threshold Lemma fails => no p>=i divides both => R_{>=i}(C(n,i)) | C(n-j,i). ROUGH-GROWTH LEMMA (the new crux): R_{>=i}(C(n,i)) ∤ C(n-j,i) for all 1<=i<j<=n/2, i.e. exists prime p>=i with v_p(C(n,i))>v_p(C(n-j,i)). OPUS VERIFICATION: 0 Rough-Growth violations to n=260; every FO triple's witness is p=i exactly (matches Cong to 1.3e8). Equivalent falling-factorial form: R_{>=i}(prod_{r=0..i-1}(n-r)) ∤ prod_{r=0..i-1}(n-j-r). STATUS: genuine verified progress -- the reduction now explicitly defeats the Bloom/StijnC objection (unlike Parthasarathy), uses only Kummer/carry bookkeeping, no prime-distribution input. #699 still OPEN; Rough-Growth Lemma unproven (it is a Sylvester-Schur-refinement: top i-block has a >=i-rough prime power the shifted block lacks; empirically airtight but not proved). NEXT: prove the Rough-Growth Lemma.

claimcomputational_search · proposer:GPT-Pro (Shift Lemma + reducti — GPT-Pro (Shift Lemma + reducticomputational_search · proposer:GPT…GPT-Pro (Shift Lemma + reductilp_dual_recompute · opus:independent(PuLP-CBC/exact) — Opus 4.8lp_dual_recompute · opus:independen…Opus 4.8

honest null

machine-sealed

#699 Rough-Growth Lemma: BOTH natural proof routes now REFUTED. The 'non-FO => p>i witness' split is FALSE -- counterexample (28,5,11) (non-FO, but only p=i=5 witnesses rough-growth; 16 such triples n<160, Opus-verified). With the earlier Bloom/StijnC Case-B refutation of the rough-part route, #699 looks like a genuine wall at the now-precisely-isolated crux.

GPT-Pro could not close the Rough-Growth Lemma and refuted the proposed Sylvester-Schur split. REFUTATION (Opus-verified): (28,5,11): C(28,5)=2^3 3^3 5 7 13, C(28,11)=2^2 3^3 5 7 13 19 23 (non-FO: 7,13>5 divide both), but C(17,5)=2^2 7 13 17 so v_7,v_13 are EQUAL in top and shifted blocks; the only rough-growth witness is p=i=5. So the threshold prime p=i is necessary even OUTSIDE FO triples -- 16 non-FO triples with no p>i witness for n<160. SHARPENED CRUX (carry form, exact): rough-growth fails iff E_p(n;i)<=E_p(n-j;i) for all primes p>=i, where E_p(t;i)=max_{0<=r<i} v_p(t-r) [and v_i(C(t,i))=E_i(t;i)-1 for prime i]. I.e. EVERY rough prime-power p^e (p>=i) of the top i-block n-i+1..n is matched to >= equal power in the shifted block n-j-i+1..n-j; equivalently p^e | (j+s-r) for some r,s in 0..i-1, absorbing it into the window {j-i+1,...,j+i-1}. Sylvester-Schur only gives R_{>i}(C(n,i)) | prod_{u=-(i-1)}^{i-1}(j+u) (verified: (28,5,14) -> 7*13 | 10..18), which is INSUFFICIENT -- the threshold prime p=i is the missing part. STATUS: #699 reduction is in its best state (Shift Lemma fix survives Case B, verified 0 viol to 260), but the Rough-Growth Lemma is a genuine wall: the two natural routes (rough-part C(j,i) -> Bloom/StijnC hole; Sylvester-Schur p>i split -> (28,5,11)) are both refuted. The crux is a precise Diophantine/carry matching statement, empirically airtight but resistant. RECOMMEND: stop trying to close unconditionally; the honest deliverable is the corrected reduction + precisely-isolated crux + the two verified refutations -- already more honest/correct than the rejected Parthasarathy proof. A clean Canopus trust-layer story: adversarial verification fixed the published proof's hole and then killed the natural closing routes with explicit counterexamples.

claimcomputational_search · proposer:GPT-Pro (refutation+crux) + Op — GPT-Pro (refutation+crux) + Opcomputational_search · proposer:GPT…GPT-Pro (refutation+crux) + Opexact_arithmetic_recompute · opus:independent(PuLP-CBC/exact) — Opus 4.8exact_arithmetic_recompute · opus:i…Opus 4.8

verified reduction

needs verification

TRANSFER MAP (TF-IDF over problem statements) fixes the isolation-audit flaw: it surfaces an UNATTENDED + OPEN cluster of binomial-coefficient-divisibility problems sitting directly on our #699/#700 Kummer/carry machinery -- #1093, #1094, #386, #849, #387 (all open, ~1 comment each). Our verified method TRANSFERS; nobody is there.

The full audits assessed problems IN ISOLATION (shape + attendedness), discarding our biggest asset: the verified techniques from problems we cracked. A TF-IDF/cosine transfer map (nearest un-worked open neighbors of each machinery win) immediately yields high-value targets the isolation audit buried: #699/#700 Kummer-carry binomial-divisibility cluster (all OPEN, ~1 comment = unattended): #386 (can C(n,k) be a product of consecutive primes infinitely often? C(21,2)=2*3*5*7), #849 (for every t, is there a with C(n,k)=a having exactly t solutions), #1093 (deficiency = #{i<k: n-i is k-smooth} -- SAME smoothness structure as our #699 Rough-Growth), #1094 (least prime factor of C(n,k) <= max(n/k,k) with FINITELY many exceptions -- a #700 sibling, finite-witness shape), #387 (sim 0.333). Other clusters surfaced: #488-multiplicity -> #52 (sumset/diff, sim 0.39), #389 (n(n+1)...(n+k-1) product); #458-lcm -> #873, #536; #306-unit-fraction -> #288, #319, #282. COMPOUNDING INSIGHT (the Vela thesis in action): cracking #699's Rough-Growth Lemma doesn't just solve one problem -- it validates the Kummer/carry/smoothness toolkit that TRANSFERS to this whole unattended cluster. NEXT: build the FULL transfer graph (embed all 1217, map the 6 machinery-techniques to clusters, surface all unattended machinery-matched targets), and attack the binomial cluster with the shared toolkit. This is the corrected frame: not cold triage, not give-up -- point verified machinery at unattended neighbors via the connection graph.

verified reduction

machine-sealed

#699 SHARP RESIDUAL + GPF-INSUFFICIENCY (GPT-Pro, Opus-verified through gate): the Window-Rough Sublemma residual is now the precise PRIME-POWER WINDOW PACKING LEMMA, and greatest-prime-factor methods are PROVEN structurally insufficient to close it. k=1,2 settled; top-prime settled; the genuinely-hard core is a short-interval CRT/carry packing statement, not a GPF bound.

GPT-Pro could not close the Window-Rough Sublemma but sharply isolated its irreducible core. SETTLED (Opus-verified): k=1,2 (0 Window-Rough failures to N=2000; clean elementary proofs); top-prime case (a prime in N-k+1..N always witnesses since P>j+k-1-r). GPF-INSUFFICIENCY (Opus-verified, structural): in the prime-free residual every top term N-r is composite so its largest prime factor <= (N-r)/2 <= N/2; at j=N/2, witnessing needs Q>N/2+k-1>N/2>=Q -- impossible. So GPF alone CANNOT close it near j=N/2. Confirmed beyond j=N/2: 18,081 triples (N<400) with prime-free top block, GPF FITS (Q<=j+k-1), yet witnessed by a threshold prime power GPF can't see -- e.g. (28,5,14): Q=13<=18 fits, but 5^2=25 (r=3) witnesses since [8..12] has only one factor of 5. EXACT REDUCTIONS: large-prime-power (p^e|N-r, p^e>j+k-1-r => p witnesses); the failure condition is the CRT packing 'forall r, forall p^e||N-r (p>=k): [j-r,j+k-1-r] contains a multiple of p^e'; near-central doubling constraint (q|delta+r-2s, delta=N-2j, so large absorbed prime powers must sit on exact-doubling positions N-r=2(j+s-r)). KNOWN GPF inputs (Laishram-Shorey P>2k for n>~k+13; Nair-Shorey P>4.42k for prime-free n>100) only settle j<=3.42k+1 -- a vanishing fraction of [k+1,N/2]. RESIDUAL = PRIME-POWER WINDOW PACKING LEMMA: prime-free top block => exists r, prime p>=k with v_p(N-r)>max_s v_p(j+s-r). This is #699's irreducible core, stripped of all settled cases. HONEST: NOT a solve; the core is a short-interval prime-power/CRT statement, likely an analytic-Diophantine wall, but now precisely named. OPUS VERIFIED: k<=2 (0 fail to 2000), GPF-blind residual nonempty (18081), (28,5,14) structure exact.

claimmanual_referee · proposer:GPT-Pro — GPT-Promanual_referee · proposer:GPT-ProGPT-Proexact_arithmetic_recompute · opus:sympy-independent — Opus 4.8exact_arithmetic_recompute · opus:s…Opus 4.8

verified reduction

needs verification

#699 Window-Rough Sublemma (prime-free residual) GPF-angle: PROVEN sub-claim Q>j+k-1 => p=Q witnesses (short Kummer proof, boundary-sharp), independently re-derived via raw base-Q carry-count (31898/31898, 0 mismatches vs max-formula in 48971 tests). Disposes the bulk region. Residual Q<=j+k-1 is NOT finite (17073 to N=300); within it, p=k-only hard cases are rare but persist; k^a>j+k-1 closes 27/36 to N=600; the irreducible 9 are a length-k window / j mod k^a residue-avoidance wall. honest grade verified_reduction + obstruction_map, NOT settled. Lemma verified 0 failures to N=350 (1.74M triples). Prompt example (28,5,11)->r=3,25 not|[8..12],p=5 reproduced.

Angle: greatest-prime-factor of top block. Verifier docs/erdos-attack/699/verify699.py. Two independent valuation methods cross-checked. Sharp boundary: Q>=j+k-1 fails at r0=0 (Q|j+k-1); 800 boundary p=Q-fails, 0 lemma-failures. Witness classes in core (N<=400): intermediate-prime 22341, p=k+others 8764, p=k-ONLY 33. The threshold prime p=k carry condition is the irreducible crux (matches prior campaign: p=k necessary outside FO triples; this is what Bloom rejected Parthasarathy 2026 on). Note docs/erdos-attack/699/WINDOW-ROUGH-SUBLEMMA-NOTE.md.

sieve+kummer cross-check, N<=350 full + N<=600 prime-free

verified reduction

machine-sealed

Erdős #699 Window-Rough Sublemma (prime-free residual): CORRECTED object + CRT obstruction, Opus-verified. The rough object is the SET/PRODUCT of all maximal rough prime-powers Q_k(m)={p^v_p(m): p>=k, p|m} (NOT the single largest; (65,3,11) discriminates — largest 13 is absorbed but 5 witnesses). Our prior R_{>=k}=rough-part (product) framing is exactly equivalent (coprime moduli) and remains sound. Window-Rough FAILS iff for every q in Union_r Q_k(N-r): N mod q < k AND (N-j) mod q < k (verified 0 mismatches / 83520 prime-free triples). Exact packing count: a single rough prime-power q>=k is incident to <=1 (r,s) pair with q|N-r and q|j+s-r, so failure is NOT a local capacity problem — it is a global CRT alignment (a Complete CRT Packing Certificate). Sharpened verified reduction plus obstruction map; not a proof. Packing alone does not close the lemma.

Witness at r exists iff rough-part(N-r) does not divide the window product prod_{s<k}(j+s-r), equivalently some q in Q_k(N-r) misses the window. (65,3,11): r=0, N-r=65=5*13, window 11*12*13; 13 absorbed, 5 witnesses -> largest-only framing is false, product/full-set is correct. CRT form: with r(q) the unique top index q|N-r(q) (unique since q>=k>|r-r'|), failure means j == r(q)-sigma(q) (mod q) for all q in the union, i.e. both N and N-j lie in the first k residues mod every maximal rough prime-power of the top block. Bad-j density <= prod_q (k/q); large-prime/top-prime cases (q>j+k-1-r) witness immediately. (28,5,14) sits in the threshold core (q=25, r=3). GPT-Pro states (and Opus confirms the obstruction is genuine) the certificate cannot be ruled out by packing alone.

claimcomputational_search · gptpro:CRT-packing-derivation — GPT-Procomputational_search · gptpro:CRT-p…GPT-Proexact_arithmetic_recompute · opus:verify_699_crt_obstruction.py — Opus 4.8exact_arithmetic_recompute · opus:v…Opus 4.8

scripts/verify_699_crt_obstruction.py -> ALL VERIFIED (0 mismatches, 83520 triples; (65,3,11)/(28,5,14) confirmed).

verified reduction

machine-sealed

Erdős #699 Window-Rough Sublemma: central-doubling exact reduction + unconditional central-strip finiteness, Opus-verified. For k>=3, M=N-j, delta=N-2j, the identity A_r-2B_s = -(delta+r-2s) (A_r=N-r, B_s=M-s) and oddness of primes p>=k give: q|A_r and q|B_s iff q|A_r and q|(delta+r-2s). Exact-doubling positions D_delta={r: delta+r even, 0<=(delta+r)/2<=k-1} impose no obstruction. Hence Window-Rough FAILS iff rough_{>=k}(N-r) | prod_s |delta+r-2s| for every non-doubled r (verified 0 mismatches vs the real witness, 99585 k>=3 triples). In the central strip 0<=delta<=k-1 the non-doubled top terms are ALL odd, so only odd primes <k can appear; m=floor(k/2) > |T|=#odd primes<k (verified all k in [3,400)), which bounds N for fixed k => FINITELY MANY failures in the central strip (unconditional). Residual = an S-unit-type system for fixed (k,delta). Sharpened reduction plus a genuine unconditional partial result, not a full proof.

Replaces the CRT near-multiple form by exact doubling. Non-doubled r with a rough prime-power q | N-r exceeding max_s|delta+r-2s| (<= delta+2k-2) witnesses immediately. Central strip: N-r odd for non-doubled r, |T|=pi(k-1)-1, m=|U_delta|=floor(k/2)>|T|, so (N-k+1)^m <= K_{k,T} N^{|T|}(3k-3)^{km} bounds N. Verified: scripts/verify_699_central_doubling.py.

claimcomputational_search · gptpro:central-doubling-identity — GPT-Procomputational_search · gptpro:centr…GPT-Proexact_arithmetic_recompute · opus:verify_699_central_doubling.py — Opus 4.8exact_arithmetic_recompute · opus:v…Opus 4.8

scripts/verify_699_central_doubling.py -> ALL VERIFIED (0 mismatches/99585; m>|T| all k in [3,400)).

obstruction map

machine-sealed

Erdős #699 Window-Rough Sublemma: the two unconditional arms PROVABLY do not meet, Opus-verified. Explicit thresholds: arm A (large-prime) closes it iff delta>=delta_A(N,k)=N+2k-1-2H(N,k) with H=max_{r,q in Q_k(N-r)}(q+r) (verified: arm A fires iff delta>=delta_A, 0 mismatches/149600 triples); arm B (central-doubling) closes it only for delta sublinear in N. A CRT construction N≡r+ell_r (mod ell_r^2) with distinct primes ell_r>k forces ell_r||(N-r), so H(N,k)<=N/L+O_k(1) and delta_A>=N(1-2/L) is LINEAR in N (verified k=3: delta_A/N=0.995, arm A fires only for j<=1.6e10 << N/2=3.35e12) while delta_B is sublinear — the arms leave a genuine intermediate band. The residual there is the exact S-unit compatibility system u_r c_r - u_r' c_r' = r'-r over non-doubled positions (R_{>=k}(N-r)|prod_s|delta+r-2s|), finite per fixed (k,delta) by Evertse-Schlickewei when m_delta>=2; the k=3 m_delta=1 edge (C_(1,delta)=3, N-1 odd) is settled. Honest obstruction map: shows the two-arm method insufficient and isolates the irreducible S-unit certificate; not a proof of the lemma.

Arm A witnesses via the DIFFERENCE window: q|N-r and q|M-s => q|(j+s-r), so q>j+k-1-r kills all differences (the lower window M-s may be large; obstruction is through the difference, not M-s size). delta_A=N+2k-1-2H. Separation: ell_r||(N-r) gives any other rough power q<=(N-r)/ell_r so H<=N/L; delta_A>=N(1-2/L). delta_B from (N-k+1)^{m_delta}<=K_{k,S}N^{|S|}D(k,delta)^{k m_delta} is sublinear. Residual = S-unit band; Evertse-Schlickewei bounds solutions per fixed (k,delta), m_delta>=2 (k>=4 always; k=3 m_delta=1 only delta=0,2 with C=3, impossible for odd N-1 large).

claimcomputational_search · gptpro:threshold-calculus+CRT-separation — GPT-Procomputational_search · gptpro:thres…GPT-Proexact_arithmetic_recompute · opus:verify_699_arm_thresholds.py — Opus 4.8exact_arithmetic_recompute · opus:v…Opus 4.8

scripts/verify_699_arm_thresholds.py -> ALL VERIFIED (delta_A formula 0 mismatches/149600; CRT separation delta_A/N=0.995; k=3 edge C=3).

obstruction map

machine-sealed

Erdős #699: pairwise S-unit uniformity for the residual is FALSE — the band needs the FULL non-doubled set, Opus-verified. Beyond the two-arm gap (att_ed9ed7479a4e00a4), the intermediate-band residual is a MOVING-TARGET divisor S-unit system: for each non-doubled r, N-r = u_r * prod_s d_{r,s} with u_r supported on primes <k and d_{r,s} | |delta+r-2s|, compatibility u_r prod d_{r,s} - u_r' prod d_{r',s} = r'-r. An explicit affine-chain family (N=3d, j=d, delta=d; r=0,r'=3, s=0,s'=2) satisfies the PAIRWISE compatibility identically (3d - 3(d-1) = 3 = r'-r, with d|C_{0,d}, (d-1)|C_{3,d}; verified over k>=4 and a range of d), so no two-position resultant / fixed-coefficient S-unit bound can give uniform finiteness. The coefficients d_{r,s} are divisors of moving linear forms in delta, so fixed-coefficient S-unit theory does not apply; a proof must rule out a GLOBAL covering of all non-doubled positions (the Uniform Moving-Target Packing Lemma). Honest obstruction map; not a proof.

Affine chain: N-r=u(delta+r-2s_r) => N=u*delta+(u+1)r-2u s_r; same N across positions needs (u+1)r ≡ C (mod 2u). The d=1 case u=3 gives N=3d, N-3=3(d-1). Verified scripts/verify_699_1093_obstructions.py. Effective levels: fixed (k,delta) finite by Evertse/Beukers-Schlickewei; uniformity over delta needs new moving-target effective input.

claimcomputational_search · gptpro:moving-target-Sunit+affine-chain — GPT-Procomputational_search · gptpro:movin…GPT-Proexact_arithmetic_recompute · opus:verify_699_1093_obstructions.py — Opus 4.8exact_arithmetic_recompute · opus:v…Opus 4.8

scripts/verify_699_1093_obstructions.py [#699] -> affine-chain family valid (ALL VERIFIED).

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is **not known** in general: it’s an **open conjecture** of **Erdős and Szekeres** (1978).

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · solved (literature)

theorem sylvester_schur (n i : ℕ) (hi : 1 ≤ i) (hi_half : i ≤ n / 2) :
    ∃ p : ℕ, p.Prime ∧ i < p ∧ p ∣ Nat.choose n i
formal-conjectures/699.lean ↗

related: #287 · #386 · #387 · #458 · #488 · #700 · #849 · #993 · #1082 · #1093 · #1094

status

open

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 3511c191850be21378d1156c045cd3ba9a4363c5d546e5beef38798bc9215eda

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.