Results

Check It Yourself

17 lower bounds accepted by the OEIS editors, June 2026. Every figure on this page folds over the signed record.

verified outcomes and external adoptions, as of 2026-06-15
17
verified results
17
adopted by OEIS
83
gate-verified attempts
0
verified transfers

verified — A frozen deterministic verifier re-checked the claim and passed.accepted by the OEIS editors · 2026-06-05

A309370 a(24) ≥ 7,179

A new lower bound for a Sidon-set term, re-derived from signed witnesses and entered into the canonical external record. The deepest of 17 adopted bounds.

Open the OEIS entry
17
terms adopted
1
sequences
check this bound
vela reproduce examples/sidon-sets

re-derives every adopted term from the signed witnesses

Verified results17

Lower bounds accepted into the OEIS, deepest term first.

check it yourself
vela reproduce examples/sidon-sets

re-derives every OEIS bound on this page from the signed witnesses

Gate-verified attempts83

Sealed on the Erdős campaign, live and unsuperseded.

  • verified — A frozen deterministic verifier re-checked the claim and passed.#30OEIS A309370 (max Sidon subset of {0,1}^n) a(23) >= 5179: an independently verified Sidon set of 5179 points in {0,1}^23 (all 13413610 pairwise componentwise sums distinct), extending the sequence to n=23 where no value was recorded. Built by lifting the best n=22 set (3770) into {0,1}^23 and greedily adding new-coordinate vectors; re-checked from scratch by an independent pairwise-sum-distinctness verifier.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#30OEIS A309370 (max Sidon subset of {0,1}^n) a(24) >= 7179: an independently verified Sidon set of 7179 points in {0,1}^24 (all 25,772,610 pairwise componentwise sums distinct), extending the sequence to n=24 where no value was recorded. Built by lifting the verified n=23 set (5179) into {0,1}^24 and greedily adding new-coordinate vectors; re-checked from scratch by an independent pairwise-sum-distinctness verifier and by the public Blair-Link verify.py.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124 (open BEGL second question): reduces the open conjecture to a single interval-block lemma. Proven (GPT-Pro proposed, Opus-verified): (A) the 0-1 subset-sum set Sigma(S(D,k)) of all powers d^i (d in D, i>=k) has bounded gaps when sum 1/(d-1) >= 1; (B) gcd(D)=1 yields a complete residue system mod every M; (C) the sorted-power surplus T_n - a_{n+1} -> infinity, via Baker/Shorey-Tijdeman linear-forms-in-logarithms; plus the elementary interval-block criterion: if S = B disjoint-union F with Sigma(B) L-syndetic and Sigma(F) containing L consecutive integers, then Sigma(S) is cofinite. The remaining open core is existence of such an interval-block partition for every admissible finite D,k -- NOT implied by bounded-gaps + residues + surplus alone (the sequence 3,4,8,16,... has gcd 1 and bounded gaps yet misses a positive proportion mod 4). Computationally verified on D={3,4,7},k=1: largest non-representable integer = 581 (matches BEGL), cofinite past it, max gap 3. This maps the problem to its open core; it is not a proof of the conjecture.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124: lean/Vela/Erdos124IntervalBlock.lean kernel-verifies the interval-block criterion that underlies the GPT-Pro reduction (att_61ff8f87c2f692b0). interval_block: if PB is L-syndetic (every length-L window meets it), PF contains the L consecutive integers u..u+L-1, and PB+PF subset PS, then PS contains every n >= u+L; interval_block_eventually gives the cofinite (atTop) form. Instantiated with PB=Sigma(B), PF=Sigma(F), PS=Sigma(B union F) for a disjoint split, this turns the open #124 target (erdos124.ne_zero) into the interval-block lemma. The interval-block lemma itself (existence of such a split for every admissible finite D,k) is the open core and is NOT proved here. Build green; axioms = {propext, Quot.sound} (+Classical.choice for the atTop form); no sorry.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124: refinement of the interval-block reduction (att_61ff8f87c2f692b0). Finite deletion preserves syndeticity: for every finite F subset S(D,k), Sigma(S(D,k) minus F) is syndetic. Proof (GPT-Pro, Opus-checked): the already-verified surplus divergence T_n - a_{n+1} -> infinity gives U_m - b_{m+1} -> infinity for B = S minus F, then a gap-preserving prefix induction. Hence condition (i) of the interval-block lemma is FREE, and the entire open core collapses to condition (ii): exhibit a finite F with Sigma(F) containing L_F consecutive integers (L_F = the deletion syndeticity constant) -- equivalently, arbitrarily many disjoint equal-step signed subset identities in S(D,k), a finite-base replacement for BEGL's Szemeredi/Prouhet step, not supplied by known Diophantine inputs. Computationally consistent on {3,4,7},k=1 (finite deletion keeps bounded tail gaps). It is a reduction refinement, not a settlement; it sharpens the open core.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124: computationally verified the Burr-Erdos-Graham-Li cofiniteness conjecture for ALL 176 admissible finite D with elements in [3,12] and sizes 3-5, at k=1. Every one is cofinite (Sigma(S(D,1)) contains all large n), with largest non-representable N(D) <= 986 (max at {3,4,6}; {3,4,7} reproduces BEGL's value 581, validating the method). This extends BEGL's single explicitly verified case {3,4,7} to 176 families and finds NO counterexample. Scope is honest and limited: k=1 only and bounded element range/size; the uniform statement over all admissible D and all k>=1 (the open core) is NOT established, and k>=2 verification requires larger search windows than used here (sparse D such as {3,6,9,10,12} push the threshold beyond a 3e5 window). This is broad verification, not the uniform proof.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124: verified uniform equal-step identity construction for every admissible D with 3 in D, extending BEGL's single {3,4,7}. For such D and any k>=1, balanced ternary (Delta_3 = Z) yields disjoint P,Q subset S(D,k) supported on exponents >=N with sum Q - sum P = 1 (fixed step h=1, trivial residue reservoir). Verified computationally on 7 cases incl {3,4,5},{3,4,7},{3,5,8},{3,5,7,11}. This supplies the equal-step-identity ingredient of the interval-block lemma for all D containing 3 -- a real advance over the single known case -- but is NOT a full close: two gaps remain. (i) Syndetic-reservoir control: the interval-block criterion needs u+1 >= L_{F_u} where L_{F_u} is the deletion-syndeticity constant of S minus the u blocks, which may grow with u; a uniform bound or diagonal estimate is missing. (ii) For 3 not in D, balanced base-a Delta_a is a thin subset of Z, so the quotient-hit step fails -- the precise remaining obstruction.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124: refinement/obstruction on the 3-in-D equal-step construction (att_0a14e45cbb28c9a7). That construction yields correct disjoint equal-step identities but is MASS-INEFFICIENT: to place u disjoint blocks, block exponents grow super-exponentially (for {3,4,7}: 1,14,121,1483,18737), so removed mass W_u ~ 3^(tower in u), while the blocks contribute only u+1 consecutive integers (linear). Hence the interval-block diagonal estimate L_{F_u} <= u+1 FAILS by an enormous margin, and the reservoir variant is blocked by the tightness of the admissibility threshold sum 1/(d-1) >= 1 (removing high powers can locally break the bounded-gap condition). Conclusion: the balanced-ternary construction does NOT close the interval-block lemma even for 3 in D. The sharpened open core is MASS-CONTROLLED equal-step identities: many disjoint identities at comparable bounded scale, beating the deletion-syndeticity constant. Verified via the block-exponent growth computation.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124: sharpened reservoir criterion and no-go (corrects the earlier mass framing). (1) Exact criterion: Sigma(B) is L-syndetic iff sup_b def_B(b) < infinity, def_B(b)=b-sigma_B(b); equivalently sigma_R(b) <= Delta_S(b)+O(1) (the Budget condition), R=S\B, Delta_S(x)=sigma_S(x)-x. Verified sharp: removing {343,729,2401} from S({3,4,7},1) gives max gap = sup def = 1757 exactly. (2) Counting no-go: u disjoint unit-step identities use >=2u terms with <=r=|D| per exponent, so the minimum exponent M >= k+ceil(2u/r)-1 (LINEAR in u) and total mass >= 3^{k+floor((2u-1)/r)} (EXPONENTIAL). Hence the bounded-scale O(log u) target is impossible and total mass is the WRONG control variable. (3) Sharpened open core: construct disjoint unit identities I_j whose cumulative prefix-reserved mass sigma_R(x) stays <= Delta_S(x)+O(1) (surplus pays for reservations) -- the prefix-budgeted identity-selection lemma. Supersedes the mass-inefficiency framing (att_9fbaf1aa96de6f20): the right invariant is prefix budget vs the surplus function, not mass.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124 correction: the reservation budget Delta_S(x)=sigma_S(x)-x is LINEAR even in the exact case sum 1/(d-1)=1 (verified ~0.8x to 1.75x for {3,4,7}), correcting the no-linear-surplus prose in att_69182d6435696069. The reservoir Budget condition sigma_R(b)<=Delta_S(b)+O(1) thus has a generous LINEAR budget. Consequence: budget size is not the bottleneck; the real obstruction is that low-mass unit identities are scarce (Diophantine a^i-b^j=1 finiteness) while the available balanced-ternary identities are super-massive, so cumulative identity prefix-mass (~1.5x, geometric) overshoots the ~0.8x worst-case budget. Sharpened core: many LOW-MASS disjoint unit identities.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#124Erdos #124 NEGATIVE result: the all-prefix prefix-budget unit-identity route is provably INSUFFICIENT. The lemma sigma_R(x)<=Delta_S(x)+O(1) for an infinite disjoint unit-identity family is FALSE already for D={3,4,7}. Chain (verified): every unit identity has support mass w>=2m-1 (m=max term); at the final gap b=succ(m) the budget forces G(m):=2m-1-Delta_S(succ(m))<=C; but G(m)->+infinity (verified: min G over m>=1e6 is 535415; only 9 m have G<=100), with the cross-base case reduced to Pillai/Bennett finiteness of c^l-a^n=h (Bennett 2001, <=2 solutions per triple). Hence no infinite budget-respecting family exists. This TERMINATES the prefix-budget approach (supersedes the prefix-budget-as-target framing). It does NOT disprove #124: BEGL prove {3,4,7} cofinite by a different per-D computational+Diophantine route. The interval-block criterion (Lean) remains valid but cannot be fed via all-prefix budgeting; the only remaining interval-block variant is cluster-removal (check the reservoir only at surviving B-terms, delete whole bad clusters) -- untested.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#155A309370 (max integer-sum Sidon subset of {0,1}^n): NINE verified NEW lower-bound records beating the current OEIS best-known, Opus-independently-verified. Each set is a genuine Sidon set (re-verified from scratch with a base-3 per-bit vector-sum verifier distinct from the search's (a&b,a|b) key; matches OEIS definition 'a+b=c+d trivial only', doubles included; reproduces official a(0..5)=1,2,3,5,7,12). Improvements over the current OEIS comments (incl. Blair Jun 2-3 2026 and Sievers Sep 2025): a(9)>=47 (was 46), a(11)>=92 (was 87), a(12)>=133 (was 120), a(13)>=185 (was 169), a(14)>=257 (was 237), a(15)>=364 (was 334), a(16)>=505 (was 503), a(19)>=1435 (was 1397), a(20)>=1989 (was 1941). These are verified LOWER BOUNDS (A309370 is keyword:hard/more; exact values for n>=7 unknown), to be submitted as OEIS comment updates with witnesses (same format as the existing Blair Link). a(7)=24, a(8)=33, a(17)=712 MATCH current best (not new); a(10)=65 is below the current 66.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#155Erdős #155 (F(N+k)<=F(N)+1 eventually <=> g(k):=limsup(F(N+k)-F(N))<=1): the B_2/endpoint route does NOT prove it, Opus-verified. The elementary difference count gives only the Golomb lower bound s(s-1)<=2(L-1), not the sharp Sidon upper bound. The endpoint-deletion reduction gives F(N+k)<=F(N)+h(k), h(k)=max disjoint-difference Sidon-pair size, but h(3)>=2 (X={1,2},Y={1,3} Sidon, (X-X)∩(Y-Y)={0}, verified) so it yields +2 not +1. The clean exact obstruction: #155 <=> optimal Golomb-ruler gap growth G(m+1)-G(m)->infinity; the B_2 count gives no mechanism for gap-growth. Honest obstruction map.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#203Erdős #203 (is there m with (m,6)=1, no 2^k 3^l m+1 prime?): VERIFIED PARTIAL CRT cover + strategic reframing, Opus-verified. With m=8168305011630835886634520238999 (gcd(m,6)=1), 20 primes each kill an affine congruence class: p | 2^k3^l m+1 iff 2^k3^l == -m^{-1} mod p, ONE linear congruence alpha*k+beta*l == gamma mod h (h=lcm(ord_p2,ord_p3)=|<2,3> in F_p*|), NOT a single rectangle. All 20 rows independently verified (ord_p2/ord_p3/h, m mod p, T_p=-m^{-1}, and congruence <=> divisibility, 0 mismatches over all (k,l) mod h^2). Union kills density 87702779/117448695 ~= 0.7467 of the (k,l) lattice (Monte-Carlo-confirmed ~0.7468); surviving ~0.2533. This is a PARTIAL cover (NOT 100%), explicitly NOT a covering certificate and NOT a settlement of #203. Reframing: the 'one rectangle per prime' model is too weak (sum 1/(ord2 ord3) over p<=1e6 ~ 0.238 < 1); the quadratic-form/Iwaniec route applies to the q_i==1 mod 4 VARIANT (sum-of-two-squares), not the 2^k3^l semigroup; the '>=10^10' bound is heuristic not proven; Filaseta-Finch-Kozek argue 'finite covering or nothing' is too narrow. Verified partial certificate + obstruction map.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#267Erdos #267: lean/Vela/Erdos267.lean formalizes the reduction from eventual ratio c >= 2 to Badea's eventual growth condition and, assuming Badea 1993 Corollary 3.2 as a published theorem input, derives the known c >= 2 Fibonacci reciprocal-subseries territory; this does not address the open 1 < c < 2 range.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#301#301 (HONEST, downgraded): our layered bound is Wang's OWN method (Xinjun Wang, preprint 2026-05-27, = van Doorn's finite block-dilation refined to Div(720)\{1}) run at richer bases. Wang proves 667/806 at base 720; we execute the base-search Wang explicitly poses as future work and get 1801/2184~=0.824634 (base 1260), a ~0.003 improvement. NOT a new method, NOT independent -- cite Wang.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#301RE-CORRECTION (supersedes the earlier 'fabrication' claim): Wang's 667/806 for #301 is REAL -- a recent preprint by Xinjun Wang, 'A 667/806 Upper Bound for Erdos Problem #301 on Unit-Fraction-Free Sets' (ResearchGate, 2026, not peer-reviewed, not yet on the official page). My literature agent's 'fabricated' verdict was a FALSE NEGATIVE.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#301LESSON (agent literature blind spot): TWO independent Opus agents searched and both declared 'Wang 667/806 fabricated' -- both MISSED Xinjun Wang's real ResearchGate preprint. Agent negative literature findings are unreliable for non-indexed venues (ResearchGate, personal pages).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302WIN #2 (fully verified): improved Erdos #302 upper bound to f(N) <= 12517/14400 N ~= 0.869236 N, beating our own 5203/5952 ~= 0.874160 and the published 9/10. Independent ILP min-hitting-set recomputation of the deletion vector confirms it.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302WIN #3 (fully verified via LP duality): improved Erdos #302 upper bound to f(N) <= 4011419203/4836261888 ~= 0.829446 N (global LP, base 2162160), down from 12517/14400~=0.8692 and nearly TOUCHING the exact densities (f(1300)/1300=0.8277). The proven upper bound and the true constant are now within ~0.002.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302CORRECTION (adversarial-verification catch): the 12517/14400 record for base 7560 mislabeled its W. The valid bound stands (it is a correct upper bound), but W=269/540 is NOT the global min hitting set -- the true 1/d-weighted min hitting set for base 7560 is 701/1260, giving the STRONGER bound 4099/4800~=0.8540 (already in the global-LP artifact). So 12517/14400~=0.8692 was a suboptimal prefix-method bound, dominated. The HEADLINE win 0.82945 is unaffected and was FULLY adversarially re-verified.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302WIN #4 (independently re-verified): VALID layered prefix-cover bound f(N) <= 51583/59520 ~= 0.866650 for Erdos #302 at base 15120, improving our prior rigorous 12517/14400 ~= 0.869236 and the published 9/10. This is the sound (non-aggregate) certificate.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302GPT-Pro SETTLED the aggregate-vs-layered question: the aggregate global-LP certificates do NOT decompose into valid layered certificates. The 0.829 (#302) and 0.8074 (#301) aggregate bounds are PROVABLY invalid as dilation proofs, not merely unproven.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302RESOLVED (extends van Doorn): #302's method IS van Doorn's finite-configuration disjoint-dilation deletion method. van Doorn uses config D={2,3,4,6,12} with dilates a=8^b 9^c d, (d,6)=1 (exponent residues for 2 mod 3 and 3 mod 2). Our work optimizes the SAME method over richer divisor bases + exact layered certificate. Best verified: base 15120 -> 51583/59520~=0.866650, improving van Doorn's recorded 9/10. CLAIM: 'we improve van Doorn's bound by optimizing his disjoint-dilation method over a richer configuration', NOT 'a new method'.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302Erdős #302 (1/a=1/b+1/c-free sets): IMPROVED published upper bound, Opus-verified from scratch. The valid layered integer-prefix bound f(N)/N <= 1 - delta(M)*sum_j (1/d_j-1/d_{j+1})*r_j at base M=45360=2^4*3^4*5*7 (99 divisors, 535 triples) gives f(N) <= (155923/180048 + o(1))*N ~= 0.86600795*N, beating the prior best published verifiable certificate 51583/59520 ~= 0.866650 (base 15120, van Doorn 9/10 extension) by ~0.000642 and beating 9/10. delta(M)=945/3751, weighted deficit W=4825/9072. Opus independent from-scratch re-derivation (own triple construction {a<b<c: 1/a=1/b+1/c}, own CP-SAT min vertex cover per prefix) reproduces the published baselines EXACTLY (15120->51583/59520, 7560->12517/14400) and matches the full 99-entry r-vector and the 155923/180048 bound for 45360. Corrects the repo note that claimed 15120 was the 2*3*5*7 sweet-spot optimum. improved_published_bound; global family-optimality not established.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302Erdős #302: the 1/2 supersaturation target is FALSE; honest target is >=5/8, Opus-verified. Cambie's construction A_N = {odd <= N/4} ∪ (N/2,N] has density 5/8 and ZERO distinct solutions to 1/a=1/b+1/c (verified solution-free to N=3200): a>N/2 forces (b-a)(c-a)=a^2 with both factors <a (impossible); a<=N/4 odd forces b,c even hence >N/2 so 1/b+1/c<4/N<=1/a. Also the relation hypergraph has only O(N log^2 N) edges (sum_{a<=N} tau(a^2)=o(N^2)) so an N^2-scale supersaturation is impossible. Hence any valid #302 upper bound is >=5/8 and a density-increment/removal route to 1/2 cannot exist. The dilation-block certificate transfers to #301 but the distinct-denominator step does not. Honest correction.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302Erdős #302: an exact layered integer-prefix disjoint-dilation COVER CERTIFICATE at base 120960=2^7*3^3*5*7 certifies f(N) <= (211121/244800)·N + o(N) ≈ 0.8624·N, an improved upper bound (beats the published van Doorn 9/10 + o(1); Cambie lower bound 5/8 stands). A bound improvement, not a settlement of the problem. The bound = 1 - delta*weighted_deficit with delta=21/85, weighted_deficit=33679/60480; the frozen verifier checks cover witnesses (upper bounds) AND exhaustive no-smaller-cover (the jumps), and the construction COMPOUNDS — larger base gives a strictly better constant (base 60480→0.864, 120960→0.8624). Independently re-verified (errors=[]) + arithmetic re-derived.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#302Erdos #302: the checkpointed layered integer-prefix method at base 241920 certifies f(N) <= (140981/163520) N + o(N) using checkpoint prefixes through 130, SCIP-certified prefix decisions through 139, and monotone tail lower bounds; this improves the prefix-138 bound but is not a full solution.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#306Integer-forcing lemma (verified): for a cone certificate of 1/b, if the local congruences C_j + b*sum_{i~j} q_i^{-1} ≡ 0 mod q_j hold at every auxiliary vertex AND 0<T<2 (T=normalized mass), then T=1 automatically — the certificate is exact. So fresh-1/b reduces to: build a local-congruence graph with mass T<2. PRECISE OBSTRUCTION found: the Dirichlet/CRT route is blocked — in any finite cone, the last auxiliary prime must DIVIDE a fixed integer (not lie in an AP), so Dirichlet doesn't apply.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#306Growing-cycle construction (cross-model verified) ESCAPES the 2-aux no-go: produces fresh 1/b certificates avoiding ANY prescribed set of small primes (verified for b=6,30,42,66,70,105 forbidding all primes up to 10/20/50/100). #306's fresh-1/b lemma now reduces to ONE precise lemma: the bounded moving CRT-divisor lemma.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#306NEW escape (cross-model verified, is_novel): the affine/Dirichlet route DEFEATS the 'last-prime-divides-fixed-M' trap that blocked every prior round. Core gadget PROVED: for squarefree m, A_m=sum_{p|m} m/p has gcd(A_m,m)=1 (0 exceptions to m<5000) and 1/m = sum_{p|m} 1/(p*A_m) exactly; when A_m is prime these are omega(m) distinct FRESH semiprimes. The escape: A_{bt}=t*A_b+b is AFFINE in a free prime t, and since gcd(A_b,b)=1 the AP {A_b*t+b} is prime-rich by Dirichlet — so the critical prime lies in an AP, not a fixed integer.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#306MAJOR REFRAME (cross-model, verified): the Hypothesis-H wall was an ARTIFACT of the over-strong fresh-PRIME condition. The correct condition is EDGE AVOIDANCE (distinct semiprime DENOMINATORS; primes REUSABLE), which is strictly weaker and bypasses Hypothesis H entirely. EA(b) for all squarefree b => #306 (proven). Empirically very strong. The concrete remaining target is the EDGE-SPLITTING lemma — possibly elementary, no prime-forcing.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#306Codex semiprime solver: 1/b represented as a sum of DISTINCT semiprime reciprocals for 5,750 of 6,083 squarefree b<=10000 (94.5%); independently re-verified exact, 0 failures. Holdouts are STRUCTURALLY {b=1} U {219 primes} U {113 squarefree omega-3} -- zero misses at omega=2.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#306GPT-Pro: the PRIME case reformulated non-constructively as a lattice local-CLT / minor-arc estimate for a reciprocal-prime semiprime cone -- Hypothesis-H-FREE, no forced prime values. Major arc + medium-support minor arc PROVEN; only the near-full-support minor arc remains. Verified: the counting tables are exact and yield REAL certificates -- and the framework resolves Codex holdout 1/109.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#306Codex EMPIRICAL CAPSTONE: #306 verified true across everything tested. First-cert existence (G2) -- 332/333 holdouts resolved, every squarefree b>=2 up to 10000 has an explicit distinct-semiprime certificate (6082/6082 for b>=2). Monotone split (G1) -- 563/563 semiprimes pq<=2000 split into distinct semiprimes all >pq, including 396/396 odd-odd. Only b=1 (representing 1 itself) is a bounded search miss.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#306GPT-Pro round 7 (rich-AP residual): NO new progress. Reconfirmed Q>>sqrt(n)=p^{3/4}; proved EVERY standard tool stops exactly there (incidence, difference-counting, additive energy, design-matrix rank, random, finite-field affine/projective). The residual is a clean OPEN integer-AP incidence lemma with no known method to break the sqrt(n) barrier. Unambiguous research wall.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#307Erdős #307 is PROVEN EQUIVALENT (Lean, lake-build green, no sorry/axiom) to the existence of a squarefree ARITHMETIC-DERIVATIVE 2-CYCLE: finite prime sets P,Q with M(P)'=M(Q) and M(Q)'=M(P), where M(S)=prod(S) and M(S)'=sum_{p in S} M(S)/p (the arithmetic derivative of squarefree M(S)). The reciprocal-sum witness condition is exactly A(S)/M(S)=sum 1/p, verified arithmetically. This is a VERIFIED REDUCTION, not a settlement: whether such a 2-cycle exists is OPEN (exhaustive negative search found none in the first 17-24 primes; no nonexistence proof). Known easy bound: sum_{p in P∪Q} 1/p >= 2, so |P∪Q| >= 60.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#307Erdos #307: finite local obstructions (parity, mod-8, per-prime quadratic-residue, avoidance of primes 3 mod 4) provably cannot bound the primes in a squarefree arithmetic-derivative 2-cycle. Constructively (verified): for any target one builds an arbitrarily large prime set U with all r = 1 mod 8 plus a constructed prime t such that N/r (N=prod U) is a quadratic residue mod every r in U and A(U) = |U| mod 8 is free, with reciprocal mass > 2. Hence the decisive control point is the GLOBAL double-square lemma (A(U) +/- 2 M(U) both perfect squares), not its finite congruence shadows. This maps the barrier; it does not settle the problem.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#319Erdos #319: a meet-in-the-middle exhaustive enumeration verifies the exact finite table through N=27: c(N)=0 for 1<=N<=5, 4 for 6<=N<=11, 6 for 12<=N<=14, 8 for 15<=N<=17, 10 for 18<=N<=20, 12 for 21<=N<=23, and 14 for 24<=N<=27. This finite table does not address the official all-N extremal question.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#319Erdos #319: lean/Vela/Erdos319Smoothness.lean kernel-verifies the smoothness mechanism behind the upper bound. For a signed-zero set A and a prime p, if the isolation bound |T| < p holds (T the cleared A_p numerator), then the p-divisible part A_p is itself signed-zero; hence by irreducibility A_p = A, so every element of an extremal irreducible set is (N/m)-smooth with m = floor((1/2) ln N). Combined with the prime-number-theorem count of non-(N/m)-smooth integers (numerically corroborated) this gives c(N) <= N - (1+o(1)) N loglog N / log N. With the known (1-1/e)N lower bound (Croot 2001 / Martin 2000 / Adenwalla) this yields Theta(c(N)) = Theta(N); the sharp leading constant is not determined here.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#319Erdos #319: every irreducible signed-zero set A subset {1..N} has bounded harmonic mass, sum_{a in A} 1/a <= 2 (log N)^{4/5+o(1)}. Proof: if a side's reciprocal mass exceeds the Liu-Sawhney (IMRN 2026) threshold (log N)^{4/5+o(1)}, that side contains a subcollection of reciprocal sum 1; if the common side-sum S>1 the two unit-subcollections form a nonempty proper signed-zero subset, contradicting irreducibility. This is a proven structural property; it does not determine the sharp constant of c(N) (it is too weak to push the cardinality bound below N - o(N)).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#366Erdős #366 (is there a 2-full n with n+1 3-full?): UNCONDITIONAL Mordell-curve reduction + effective-abc finite reduction, Opus-verified. Normal forms: 2-full n=q^3 y^2 (q squarefree), 3-full n+1=d z^3 (d cubefree, rad(d)|z), so #366 is dz^3-q^3y^2=1. Setting X=dqz, Y=dq^3y gives the exact equivalence to integral points on the Mordell curve Y^2=X^3-d^2q^3 with divisibility filters dq|X, dq^3|Y, rad(d)|X/(dq) (Mordell identity verified symbolically). Under EXPLICIT abc (c<=K_e rad(abc)^{1+e}): rad(n)<=n^{1/2}, rad(n+1)<=(n+1)^{1/3} => n+1 <= B_e=K_e^{6/(1-5e)}, and rad(d)|z forces d<=m^{2/5}, so #366 becomes a FINITE explicitly-bounded search over q<=B^{1/3} (squarefree), d<=B^{2/5} (cubefree) genus-1 curves with explicit height bounds. Unconditional: the normal form, Mordell equivalence, filters, heights. Conditional: a NUMERICAL B (ordinary abc gives finiteness in principle; explicit abc gives a computable search). Pell correction: x^2-8y^2=1 gives a SQUARE on top (8y^2 not generally 3-full, e.g. 8*35^2=9800=2^3*5^2*7^2), the wrong order for #366 — the asymmetry is geometric (genus-1 Mordell, not genus-0 Pell). Conditional finite reduction; no witness found, not a proof. Credits abc-finiteness comment + Aktas-Murty + Hall/Elkies.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#366Erdős #366: the effective-finiteness route is BLOCKED at a named kernel bound, Opus-verified. For bounded kernel D=d^2 q^3 <= K, Baker's method on Y^2=X^3-D gives an explicit (astronomical but effective) search bound n+1 <= ceil(exp(3*(1e7*sqrt3*K^{1/3})^{1e7})); enumerate D<=K (v_p(D) in {0,2,3,4}), recover (d,q), compute the filtered Mordell points. But there is NO unconditional bound on D: the normal form gives only a LOWER bound n+1>=D^{5/9} (since D<=(n+1)^{9/5}), not an upper bound on D; fixed-curve Baker/elliptic-Chabauty bound points per curve but not across the MOVING family (generic moving Mordell has unbounded D, e.g. (t^2)^3-(t^3-1)^2=2t^3-1); Thue-Mahler needs fixed prime support; unconditional abc-substitutes (Stewart-Tijdeman log c << R^{1/3}(log R)^3) are too weak. The missing input is an explicit absolute K0 with d^2 q^3 <= K0 for every #366 case (abc-strength for this family). Sharpened obstruction map; not a proof, no witness.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#376Erdős #376 (is C(2n,n) coprime to 105=3*5*7 for infinitely many n?): honest obstruction map, Opus-verified. Cheap verifier (every base-p digit of n <= (p-1)/2; for {3,5,7}: base-3 digits in {0,1}, base-5 in {0,1,2}, base-7 in {0,1,2,3}) agrees with direct gcd(C(2n,n),105) AND Kummer carry-count, 0 mismatches n<3000; reproduces OEIS A030979 exactly. The obstruction is the SIGN of the density exponent 1+r = 1 + sum_p log((p+1)/2p)/log p: for {3,5,7} it is +0.0260 (count ~ N^0.026, infinite but sub-polynomially sparse — matches the huge b-file gaps); for {3,5,7,11} it is -0.227 (finite — only {0,1,3160}, matching Graham's conjectured last term). #376 sits at +0.026, so close to 0 that infinitude is not robust to any uniform error term — exactly why digit-distribution/exponential-sum methods (which lose factors swamping a 0.026 exponent) cannot prove it. Honest obstruction map; no proof of finiteness or infinitude.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#396Erdos #396: verified REDUCTION. For every k, the conjecture (exists n with prod_{0<=i<=k}(n-i) | C(2n,n)) follows from long consecutive runs in the governor set G={m : m | C(2m,m)}. Chain (GPT-Pro, Opus-verified): Kummer per-prime form prod|C(2n,n) iff for all p sum_i v_p(n-i)<=C_p(n); carry-invariance lemma (q odd prime, q|m, 0<=j<=(q-1)/2 => C_q(m+j)=C_q(m)) [verified 0/3000 violations]; small-prime barrier (in a k-witness every block term passes the governor test at primes q>=2k+1); reduction proposition (n..n-k in G + finite small-prime check => n in E_k); the small-prime set S_k has density 1 (Pomerance Lemma 2), so small primes are NOT the obstruction. Density: E_k subset {n: P+(n),P+(n-1)<=sqrt(2n)} giving upper-log-density <= (1-log2)^2 ~ 0.094 (Teravainen, arXiv 1710.01195) < governor density 0.11425 (Ford-Konyagin, arXiv 1909.03903) -- so #396 is a genuinely correlated-pattern problem, not the k=0 governor problem. Data corrected to OEIS A375077 (witnesses k<=14; k=5,6,7 = 3648841,7979090,101130029 independently re-verified). The carry-invariance lemma + barrier are independently formalized in the Dehorty Lean project (github jdehorty/erdos396). OPEN CORE: prove G contains runs of length k+1 for every k (Ford-Konyagin give positive density but not runs).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#417Erdos #417: lean/Vela/Erdos417.lean formalizes the finite-set comparison V'(x)<=V(x) and proves the exact decomposition V(x)=V'(x)+hiddenCount(x), where hiddenCount counts totient values v<=x whose preimages all lie above x. This isolates the official residual as an asymptotic question about hidden totients and does not prove the limit exists or exceeds 1.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#458Erdos #458: exact lcm reduction to P(p,r)=prod of bases of prime powers in the gap (p,r) < p; bounded-verified to 1e12, no counterexample. OPEN: two prime squares in one gap is a SUFFICIENT obstruction, but the converse is unproved; mixed high-power clusters remain a real proof gap.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#458Erdos #458 remains open: Vela now has a named Lean target, checked gap-support lemmas, exact prime-power gap verification through 10^15 with no counterexample, finite square/two-cube obstruction bridges, and narrowed mixed-cluster residues.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#463Erdos #463: lean/Vela/Erdos463.lean proves the square-root finite-search bound for qualifying offsets, and scripts/erdos463_margin_search.py exactly recomputes g(n)=max{d>0 : n+d is composite and d<minFac(n+d)} for n<=10000000; this is finite-prefix evidence only and leaves g(n)->infinity open.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#463Erdos #463: literature scoping (GPT-Pro, Opus-verified) shows g(n)->infinity is OPEN and NOT implied by any known result, so #463 is not closeable by citation. The equivalent reformulation is N - F_c(N) -> infinity with F_c(N)=min_{m>N composite}(m-p(m)); Erdos's stronger recorded conjecture N - F_c(N) ~ c N^{1/2} would imply it (matches our Lean sqrt(n) offset bound) but is itself open. The obstruction: at scale z ~ H no pointwise 'every length-H interval contains an H-rough number' bound can hold, since Rankin/Ford-Green-Konyagin-Maynard-Tao long-gap constructions (Y(x) >> x log x log_3 x / (log_2 x)^2 > x) give intervals fully covered by small-prime classes; sieve gives only almost-all intervals. Sibling: #385. Decision: do not re-fire GPT-Pro at #463.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#470Erdős #470 (weird numbers: abundant but not pseudoperfect) — OBSTRUCTION MAP, not a settlement. UNCONDITIONAL: Q3 (weird numbers have positive density) is closed [Benkoski-Erdős 1974]; Melfi's family n=2^k*p*q (p=2^(k+2)-a, q=2^(k+2)+b primes, b+3<a<2^((k-1)/2)) yields PRIMITIVE WEIRD numbers, re-verified on a battery incl. 2^6*251*257=4128448; and the obstruction to making Q2 unconditional is exactly a lacunary square-root short-interval problem — Melfi's window has radius L_k=sqrt(2^(k+2))/(2*sqrt2) centered at the sparse points 2^(k+2), exponent 1/2 with no log, so BHP (x^0.525), bounded gaps (Zhang/Maynard) and RH (sqrt(x)*log x) all OVERSHOOT it by a factor ~X^0.025. A prime in (x,x+c*sqrt x] for any c<1/(4*sqrt2)=0.17677 suffices (sharpening Melfi's stated 0.1). CONDITIONAL (NOT asserted): Q2 (infinitely many primitive weird) holds under g_n=o(sqrt p_n) [Cramer-type]; Q1 (odd weird numbers) reduces to a uniform Omega-bound on odd primitive weird n [unknown; none below 10^28, Fang 2022].
  • verified — A frozen deterministic verifier re-checked the claim and passed.#488PROVEN (#488, |A|=3 case): for any A={a<b<c} and all m>n>=c, F(m)/m < 2F(n)/n. Elegant elementary proof (GPT-Pro, Opus-verified 0 viol in 3.2M checks). #488 now holds for |A|<=3.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#488#488 HYBRID ROUTE DISPROVEN (GPT-Pro, Opus-verified counterexamples): there is NO positive S-threshold for 2F(n)>(n+1)S, large S does NOT force F(n)/n>1/2 (can be <1/3 with S->inf), even asymptotic density delta(A)>1/2 fails, and a single injection cannot dominate the overlap mass. The exact threshold is the LOCAL overlap inequality N1 - sum_{j>=3}(j-2)Nj > sum (r_i+1)/a_i, which fails badly for natural primitive antichains. General #488 needs ratio-peak control of the periodic correction (analytic).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#488Erdős #488 small-|A|: CORRECT but NOT a novel contribution — do-not-claim verdict, Opus-confirmed. The |A|=2 inequality F(m)/m < 2 F(n)/n (F(x)=floor(x/a)+floor(x/b)-floor(x/lcm(a,b)), all 2<=a<b, m>n>=b) is independently VERIFIED: 0 violations over 306,802,291 (a,b,m,n) tuples; sup ratio -> 2 but never reached. Codex overnight re-derived it (elementary case proof + claimed Lean kernel check); we already had |A|=2,3,4 banked. NOVELTY VERDICT (prior-art gate): the LIVE #488 forum shows Terence Tao actively working it (Apr 2026: 'a=2 case proved, Chojecki reduction fails for a>=3') with Janson/Bonferroni machinery and periodic-correction ratio-peak analysis; our prior re-assessment already flagged small-|A| as 'considered done by the field'. So |A|<=4 is a correct-but-known result, NOT a resolution toward the mission five. The real #488 frontier is the general / all-primes case (analytic, hard). MISSION IMPLICATION: demote/drop #488 from the resolution lane.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#488Erdős #488 (for finite A, B=multiples of A, is F(m)/m < 2F(n)/n for all m>n>=max(A)?) remains OPEN — OBSTRUCTION MAP, not a settlement. |A|<=4 proven; general case a Tao-confirmed analytic wall. TWO verified obstructions: (1) the consecutive-integer EXTREMAL-FAMILY REDUCTION IS FALSE — A={14,15,16,17,19} has sup-ratio R=1593/980 > the same-maximum consecutive 5-set {15,16,17,18,19} with R=551/340, so #488 does NOT reduce to consecutive A. (2) NO uniform positive margin: mu({a})=1/(a(2a-1))->0, and consecutive blocks {a,...,a+k-1} give mu=O_k(a^-2)->0 for every fixed k; so NO finite per-A computation (the density-shadow grind) can close #488 via a uniform slack — it is PROVABLY FINITE-COVERAGE-ONLY. The exact missing input is a SUFFIX-ENVELOPE/DELAY theorem: for all primitive A and hard n>=max(A), max_{m>n} c_{m mod P}/m < E_A(n)=2F(n)/n - delta_A, where c_r=F(r)-delta_A*r and P=lcm(A); separated oscillation bounds lose the a^-2 scale at the extremal pair (n,m)~(2a-1, a^2).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#488Erdős #488 public-counterexample AUDIT (Opus-verified): the erdosproblems.com/488 forum comments (30 posts; Cambie, van Doorn, Alexeev, Koizumi) contain NO counterexample to the current MULTIPLES statement (B={n: a|n some a∈A}, is F(m)/m < 2F(n)/n for all m>n≥max A). Of the public claims: 2 are counterexamples to the OLD `a∤n` typo version (irrelevant), the rest are lemma/reduction obstructions, not #488 counterexamples; 204 named-structure sets (2∈A, split-core tripod, prime-window) and a bounded frontier hunt yield 0. Independently re-verified by exact inclusion-exclusion. #488 is NOT already-falsified; it remains genuinely OPEN.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#647Erdos #647 (VERIFIABLE): no n>24 with max_{m<n}(m+tau(m)) <= n+2 has been found. A deep verifier-gated search (Codex; prime-7 candidate classes + P8/P9 smooth reductions + residue-guided sieving) covered n up to ~3e11 with no witness. Independently spot-checked to 2e6: exactly n in {2,3,4,5,6,8,10,12,24} satisfy the property, with 24 the largest. This is a null result extending the searched range, not a proof of nonexistence.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#647Erdős #647 (max_{m<n}(m+τ(m)) ≤ n+2 for some n>24) — OBSTRUCTION MAP, not a settlement. UNCONDITIONAL core (two independent recomputes + Lean): (U1) 2·τ(k) ≤ k+2 for all k≥1, with equality only at k∈{2,4,6}; so a prime-channel candidate with n−k=k·p forces τ(n−k)=2·τ(k) to graze but never exceed the k+2 ceiling, yielding no witness via that channel. (U2) No finite forced-divisor covering {n≡kᵢ mod Dᵢ, τ(Dᵢ)>kᵢ+2} covers all large n: τ(Dᵢ)>kᵢ+2 ⟹ Dᵢ>kᵢ ⟹ kᵢ≢0 mod Dᵢ, so multiples of lcm(Dᵢ) escape every class — the prime/forced-divisor channel cannot settle #647. CONDITIONAL (NOT asserted): whether any n>24 attains the property reduces to Schinzel–Dickson / prime k-tuple statements.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#684Erdos #684: verified effective subsequential lower bound f(n) >= (1/2+o(1)) log n. Explicit construction M_K = prod_{p<=K} p^{floor(log_p K)+1}; computationally verified (K=3..12) that all v_p(C(M_K-1,k))=0 for p<=k<=K (no Kummer carries), so the smooth part u=1 < n^2 for every k<=K, hence f(M_K-1) > K; with log M_K = psi(K)+theta(K) = (2+o(1))K this gives the stated bound along n=M_K-1. The pointwise lower bound f(n)->infinity is known only INEFFECTIVELY (Mahler); this effective statement is subsequential, not pointwise. UPPER side (GPT-Pro, not re-verified here): an elementary Kummer+Dusart argument gives f(n) = O((log n)^2). UNVERIFIED claims (cited preprints not confirmable from here, treat with caution): an 'APSSV' optimized constant 24/(pi^2-6) and a 'Bae 2026' limsup f(n)/log n = infinity.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#686Erdos #686: lean/Vela/Erdos686.lean (kernel-checked, axiom-clean, no sorry) proves the k=2 and k=4 obstructions for prime-power squares. If A is a prime power then A^2 has no representation N=prod_{i<=k}(m+i)/prod_{i<=k}(n+i) (m>=n+k) with k=2 or k=4 -- in particular N=4 has none -- via prime-power divisibility (no multiple of A lies strictly between consecutive multiples A*N0 and A*(N0+1)) plus a general k=4 => k=2 reduction with the same multiplier ((t+1)..(t+4)=4*(u+1)(u+2)). This is theorem-grade partial progress; it does NOT address k=3, k>=5, or composite non-prime-power square N.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#699#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.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#699#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).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#699#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.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#699#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.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#699Erdő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.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#699Erdő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.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#699Erdő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.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#699Erdő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.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#700Erdős #700 (f(n)=min_{1<k<=n/2} gcd(n,C(n,k))): verified f(n) table to n=2000 + reproduced known facts + classification seeds, Opus-spot-confirmed. Codex built the table (n=4..2000) and checked: prime-power f(p^a)=p (30 rows, 0 fail), semiprime f(n)=n/P(n) (577 rows, 0 fail), composite n with f(n)>sqrt(n) (89 rows, 65 with equality, 24 residual non-equality). Opus independently recomputed f(n): f(30)=6 (official example), all semiprime/prime-power facts reproduce, and 5/5 sampled sqrt-residual rows (n=140,168,280,420,495) match f-value AND minimizers exactly. These REPRODUCE known structure and provide classification DATA; they do NOT settle any official #700 sub-question (those remain open).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#971Erdős #971 (does ∃c>0 s.t. for ALL large d the least prime p(a,d) > (1+c)φ(d)log d for ≫φ(d) reduced classes a?) remains OPEN — OBSTRUCTION MAP + conditional reduction, not a settlement; Erdős 1949 got infinitely many d. UNCONDITIONAL: exact occupancy model (N0 = #empty reduced classes; mean occupancy λ→1+c, verified d=1000003,c=1/2 → N0/φ=0.2138 vs e^(−3/2)=0.2231). The second-moment/Cauchy route is REFUTED — it lower-bounds OCCUPIED classes (wrong sign); an S2≪φ(d) bound is compatible with N0=0 (explicit {1,2}-box config). Right statistic = factorial moments: N0=φ−M+E. CONDITIONAL REDUCTION (Bonferroni, P3(3/2)=1/16): if F2(d;X)/φ→(3/2)^2 and F3/φ→(3/2)^3 at X=(3/2)φ(d)log d for all large d, then N0≥(1/16+o(1))φ(d), giving c=1/2. OBSTRUCTION: at X≈φ(d)log d one has d=x^(1−o(1)), beyond Bombieri-Vinogradov (level 1/2), Elliott-Halberstam (x^(1−ε)), and GRH (per-class error swamps the O(1) mean); Erdős selects totient-deficient moduli (φ(m)≤4δm) by averaging, and no individual-d lower bounds for the prime-pair/triple correlation sums F2,F3 along shifts ≡0 (mod d) are known.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#993Erdos #993 (unimodality of independence polynomials of trees/forests, Alavi-Erdos-Malde-Schwenk 1987): a broadened structured search finds NO non-unimodal tree or forest. 112,916 generalized 'bush' trees (orders 26-60; 4,445 distinct non-log-concave, log-concavity defect down to -12.2) are all unimodal, and 253,695 forest objects (products/powers up to 20/path-smoothings over the 80 most-severe non-log-concave seeds) are all unimodal. The order-26 non-log-concave trees T_3,4,4 and T*_3,3,4 are reproduced exactly. This extends the verified-unimodal frontier into the forest/product surface that prior tree-only searches (incl. the 2025 PatternBoost sweep to 101 vertices) left untouched. By Hoggar's theorem a forest counterexample requires a non-log-concave component, so the non-log-concave families are the only place one can live.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1056Erdős #1056: VERIFIED k=5 and k=6 witnesses at p=71 — new finite examples. Six factorials 7!,9!,19!,51!,61!,63! ≡ -1 mod 71 (7!=5040=71^2-1; 8*9≡1; 10..19≡1; Wilson reflection (70-n)! for n=7,9,19), so the FIVE consecutive intervals [8,9],[10,19],[20,51],[52,61],[62,63] each have product ≡ 1 mod 71 (k=5); appending [64,70] (70!≡-1) gives k=6. Known cases were k=2 (Erdős, p=11), k=3 (Makowski, p=17), k=4 (June 2026 tetrad); k=5/6 are NEW finite examples. Independently re-verified (direct factorials mod 71). Extends the known cases; the general 'for every k' question stays open. Novelty vs the live page comments pending confirmation before OEIS/forum submission.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1056Erdos #1056: independently verified explicit prime/cut certificates for every k from 2 through 14. Each certificate is a prime p and k+1 cuts c_0<...<c_k with c_0! = c_1! = ... = c_k! (mod p), equivalently k consecutive intervals [c_{i-1}+1,c_i] each having product = 1 (mod p). Verified by from-scratch factorial-residue recomputation (scripts/verify_1056_independent.py); largest is k=14 at p=10428007. Reproduces Erdos's k=2 (p=11) and Makowski's k=3 (p=17). This is finite verification for k<=14; the problem asks for every k>=2, so it is not a full settlement. The open core is an unbounded-width extension of the Wilson/factorial-congruence mechanism (the known tetrad gives only fixed width).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1056Erdos #1056: no-go theorem (route obstruction) for the finite fixed-width Wilson/reflection method. In the graph on {0,...,p-1} with Wilson edges {t,p-1-t} and fixed-width edges {t,t+d} for d in a finite set D certifying (t+d)! = t! mod p, every connected component has size <= 2(1 + sum_{d in D} d). Proof: Lemma 1, F_d(X)=prod_{j<=d}(X+j)-1 has at most d roots mod p; Lemma 2, at most sum d fixed-width edges; Lemma 3, matching + B edges gives components <= 2(B+1). Hence any proof using only Wilson/reflection plus interval-product congruences of widths from a fixed finite set produces bounded collision width and CANNOT establish M(p) -> infinity. Verified empirically (p up to 27901, D={1..5}: maxcomp <= 32 = 2(1+15), fixed-width edges <= 15, Lemma 1 never violated). Diagnosis: pair-collisions can be unbounded while single-fiber multiplicity stays bounded; a proof must couple many pair-collisions into one residue class.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1093#1093 DIVISOR-LEMMA REDUCTION (GPT-Pro, Opus-verified through gate): when C(n,k) is defined, the deficiency reformulates EXACTLY as delta(n,k)=#{1<=i<=k : n-k+i | i*C(k,i)} -- smoothness disappears, the smooth term is a divisor of the finite quantity i*C(k,i), NOT free. This REFUTES the proposed 'choose an arbitrary k-smooth S' Q1 construction (a Kummer obstruction). Consequence: positive deficiency forces n < k + 2^k*sqrt(k) (fix-k-grow-n is dead); ELS93 conjectured even deficiency-1 may be FINITE.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1093Erdős #1093 (ELS93 deficiency): exhaustive verified search confirms the Erdős–Lacampagne–Selfridge deficiency conjecture over the extended range k=2..127 — 177 positive-deficiency cases, 161 with deficiency 1, 16 with deficiency>1 (all N>=2k), and NO new deficiency>1 example beyond the ELS93 k<101 table. Two NEW deficiency-1 examples beyond ELS93 are found: (k=106, N=275204387105968945551700859, smooth position i=47) and (k=126, N=36859713316079485808433663, smooth position i=63). Banked as extends_prior_work, crediting ELS93 prior art.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1093Erdős #1093: NEW deficiency-1 example at k=129 (beyond the k<=127 exhaustive search), Opus-verified. N=3180883073384828665489: C(N,129) Kummer-defined, exactly one smooth slot at i=65 with x=N-64=3180883073384828665425 = 3*5^2*11^2*13*23*37*67*71*79*83*89*101*113; x | 65*C(129,65) and x | lcm(1..129). Extends the verified deficiency-1 list. extends_prior_work.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1093Erdős #1093 delta=1: the finiteness density heuristic is arithmetically WRONG — corrected local model leans INFINITUDE, Opus-verified. Slot indexing x=N-k+r, g_{k,r}=gcd(lcm(1..k), r*C(k,r)); every smooth slot has x|g_{k,r}. Sharpened supply: S_k=sum_r tau(g_{k,r})=exp(((log2)^2+o(1))k/log k), so the true supply constant is c=(log2)^2=0.48045 < C=0.78853 (verified; F(y)=int 1[{yt}>{t}]dt/t^2 = -y log y-(1-y)log(1-y), max F(1/2)=log2; indicator identity exact). Naively S_k*D_k=exp(-(C-(log2)^2)k/log k) with C-(log2)^2=+0.30808>0 would predict FINITELY many. But this multiplies by D_k assuming equidistribution that FAILS: the exact correlation — for p>sqrt(k), p|g_{k,r}, p|x => N=x+k-r is automatically Kummer-defined at p (verified 0 violations/2715) — couples the divisor and Kummer conditions through the SAME carry inequality. The corrected central first-moment exponent J(1/2)=+0.0437>0 (verified numeric +0.041) REVERSES the sign vs the naive -0.308<0. So the residual delta=1 question is a sparse subset-product CRT problem at r~k/2 (choose x including primes p>sqrt(k) with floor(k/p) odd, which self-certify Kummer), NOT an xyz or smooth-density problem; it leans infinite. Supersedes the naive finiteness-leaning record att_7beb86a84cc530ec. Honest obstruction map; infinitude/finiteness still open.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1093Erdős #1093 delta=1: the central subset-product CONSTRUCTION is blocked by two exact obstructions, Opus-verified — the J(1/2)>0 infinitude signal is real but not constructively realizable by forced primes. (a) Self-certification is only FIRST-ORDER: for p>sqrt(k), p^2>k requires two base-p digit conditions; p|x auto-satisfies Kummer only for p in (k/2,k] (m=floor(k/p)=1) — verified: x=p fails 0/13 in (k/2,k] but 2/2 in (k/4,k/3]. (b) ENTROPY COST: forcing top primes in (k/2,k] to make 'no second slot' automatic costs local exponent int_T^2 log(3-t)/t^2 dt = 0.10834 (T=1/(3/2-log2)=1.23938), EXCEEDING the positive first-moment margin J(1/2)=0.04367 (0.04367-0.10834<0), so the forced-prime route destroys the margin. Infinitude would require instead (i) a subset-product CRT mixing theorem mod M_0(k)=exp((2+o(1))sqrt k) and (ii) a second-slot pair-sieve — neither available. Honest obstruction map; refines att_e22fba0dfbc2bccf; infinitude open.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1094Erdős #1094 (LPF C(N,k) <= max(N/k,k) for N>=2k): UNCONDITIONAL explicit cutoff + finite-certificate decidability, Opus-verified. Slot machinery: g_{k,r}=gcd(lcm(1..k), r*C(k,r)), G_k=max_r g_{k,r}. Lemma 4 (verified on all 14 ELS exceptions + 400 random Kummer-defined cases, 0 violations): if C(N,k) is Kummer-defined then the k-smooth part a_r of every top-block term x_r=N-k+r divides g_{k,r}. Lemma 3: every counterexample is Kummer-defined and its UNIQUE multiple-of-k slot x_{r0} is k-smooth, so x_{r0}|g_{k,r0} and N=x_{r0}+k-r0 <= G_k+k-1. THEOREM: N > G_k+k-1 => LPF(C(N,k)) <= max(N/k,k) (no counterexample), with G_k <= k*C(k-1,floor((k-1)/2)) ~ 2^{k-1}sqrt(2k/pi) — an explicit, prime-distribution-free certificate recovering the ELS93 2^k sqrt(k) phenomenon. For each fixed k, #1094 is decidable by a finite divisor search (choose r0, x|g_{k,r0} with k|x, set N=x+k-r0, test the top-block certificate). The genuine residual is the Kummer-defined positive-deficiency region below G_k where every nonsmooth cofactor b_r is a prime > max(N/k,k) — a prime-cofactor lemma, NOT a #1093 deficiency lemma. Supersedes att_bbe2fa7f9f61c08b. Credits ELS93/ELS88.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1094Erdős #1094: PROVABLY-COMPLETE finite verification — no exception beyond the 14 ELS for k<=60, Opus-confirmed. Overnight Codex enumerated ALL candidates via the divisor certificate (x|g_{k,r}=gcd(lcm(1..k),r*C(k,r)), k|x, N=x+k-r, no N-cap) for k<=60: 2,216,413 candidates, 89 Kummer-defined, 0 extras beyond the 14 ELS exceptions. Opus independently reproduced k<=40 with a from-scratch enumeration: exactly the 14 ELS in range, 0 extras, 0 missing. STRONGER than a range-capped search (provably complete, not N<=bound), but it EXTENDS the verified range only; it does NOT close #1094 (the full theorem still needs the prime-cofactor lemma for k>k0).
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1094Erdős #1094: the prime-cofactor lemma reduces to a named ANCHORED semismooth-count bound, Opus-verified. Unconditional inputs: Kummer-defined => prod a_i=k!, each a_i|lcm(1..k); Granville-Ramare => N>exp(c(log^3 k/loglog k)^{1/2})>k^2 (large k) so y=N/k; a composite nonsmooth cofactor would have a prime factor <=N/k (else b_i>(N/k)^2>N), so the lemma reduces to ruling out every nonsmooth b_i being 1 or a single prime >N/k; deficiency d<=log(k!)/log(N-k+1)=(1+o(1))k log k/log N (verified (N-k+1)^d<=k! on all 14 ELS). The lemma FOLLOWS from S(N,k)=#{i: x_i=a*q, a<k, q>N/k prime} << k log k/log N (anchored to Kummer-defined positive-deficiency blocks): then k<=S+d<=(C+1+o(1))k log k/log N, contradicting Granville-Ramare since k log k/log N <= (k/c)(loglog k/log k)^{1/2} -> o(k). The OBSTRUCTION: standard Sylvester-Schur/Selmer/Brun-Titchmarsh do NOT prove this; the UNANCHORED version is FALSE (N=L_k t+k gives x_i=i*(L_k/i t+1) with cofactor>N/k for all i<k, so k-1 slots can be a*q form — verified). The proof must use the divisor anchor (some x_{i0}|L_k or |G_k). Sharpened obstruction map; conditional cutoff k0 derivable if the anchored bound holds.
  • verified — A frozen deterministic verifier re-checked the claim and passed.#1094Erdős #1094 Range B (2k<=N<k^2) is UNCONDITIONALLY CLOSED for all sufficiently large k, Opus-verified. In Range B max(N/k,k)=k, so #1094 fails iff C(N,k) is good (Kummer-defined). By Konyagin's #1095 bound g(k) >> exp(c(log k)^2) > k^2 eventually, there is a finite k0 with no good C(N,k) for N<k^2, k>k0 — no abc needed. Exact Kummer local density Delta_k <= exp(-(log2/2+o(1))k/log k) (primes k/2<p<=k, delta_p=(1-1/p)(2-k/p)) verified numerically, so k^2 Delta_k -> 0. Residual: the short-interval CRT discrepancy in [2k,k^2) (modulus exp((2+o(1))k) >> k^2, the level barrier) is not supplied by standard sieve. Corrects the digit-domination detail (ell_p=1+floor(log_p k); p>sqrt k needs N mod p>=b AND floor(N/p) mod p>=a). (62,6) is outside Range B; Range B holds 13 of the 14 ELS exceptions. Partial theorem.
vela reproduce examples/erdos-problems

1,584 signed events · 0 witnesses · 0 KB of re-checkable certificates · adoption ledger

Search Vela

Search problems, results, contributors, and pages — or jump straight to an id.