{"items":[{"id":138,"title":"van der Waerden numbers W(k)","prize":"$500 (for improving bounds / proving W(k)^{1/k} -> infinity)","statement":"Improve the bounds for the 2-color van der Waerden number W(k) (least N such that every 2-coloring of {1..N} has a monochromatic k-term AP); headline: prove W(k)^{1/k} -> infinity.","finite_object":"A 2-coloring of {1,...,N} with no monochromatic k-term AP (lower-bound witness), or a DRAT UNSAT certificate that none exists at a given N (exact value).","current_record":"Exact: W(2,3)=9, W(2,4)=35 (Chvatal 1970), W(2,5)=178 (Stevens-Shantaram 1978), W(2,6)=1132 (Kouril & Paul 2008, SAT+FPGA). W(2,7) unknown. Best lower bounds: W(2,7)>=3703, W(2,8)>=11495, W(2,9)>=41265, W(2,10)>=103474 (Ahmed et al. 2014 / Kouril / Heule SAT colorings; refined by D. Monroe 2023 SLS). Asymptotic frontier: Green 2021, w(3,k) >= k^{b(k)}, b(k)=c((log k)/log log k)^{1/3}, later sharpened - algebraic, not computational.","beatable":"WALL","beatable_reason":"Two finite sub-problems, both walled. (1) Exact-value extension: only W(2,3..6) known (W(2,6)=1132 needed clusters+FPGAs); W(2,7) ~ 10^4-10^5, so an UNSAT+DRAT cert at that N is astronomically infeasible - identical to the R(5,5) upper-bound wall. (2) Lower-bound record colorings ARE a live SAT/SLS problem with a trivial verifier, but the records are held by exactly the tools we'd use (tuned stochastic local search: Ahmed 2014, Heule, Monroe's 2023 DDFW linear-weight-transfer solver built specifically to crack these instances). No verifier moat (checker is commodity), DRAT-nonexistence infeasible, and any gain is a marginal, non-prize nudge won only by out-tuning SLS specialists. No edge beyond generic compute.","fit_score":6,"impact_score":5,"impact_reason":"Famous, central Erdős/Ramsey-theory quantity with high field significance, but the reachable piece is only a marginal lower-bound record (non-prize), the $500 prize itself requires an unreachable asymptotic theorem, and real-world relevance is negligible.","verifier":"Poly-time exact: scan a candidate coloring for a monochromatic k-AP in O(N^2/k). Trivial and cheap - but it is a commodity every prior record-holder already runs, so no moat.","attack":"Only movable target is a lower-bound record: run farm-scale stochastic local search (DDFW/yalsat with linear weight transfer, or CDCL-with-restarts) on the CNF \"2-color {1..N}, no mono k-AP\" to find a valid coloring at N above the current record for some k; verify by AP scan. Rough compute: farm-weeks of restarts per candidate k, competing head-to-head against purpose-tuned specialist solvers. Exact-value W(2,7) (UNSAT+DRAT) is out of reach at N~10^4-10^5.","our_edge":"None beyond generic compute. The record is held by exactly our toolset (tuned SLS SAT solvers); no unique verifier and no feasible DRAT-nonexistence angle.","verdict":"PARTIAL. Prize/headline (W(k)^{1/k}->infinity) is asymptotic = NONE; the genuine finite sub-problem (record colorings / exact-value extension) exists and maps cleanly onto a SAT-witness farm with a cheap exact verifier, but is practically at the WALL: exact extension infeasible, and lower-bound records are a saturated SLS arms race held by our own tools with no moat and only non-prize gains. Do not pursue.","lane":"witness-local-search","board_class":"READY","board_class_reason":"witness = 2-coloring of [N]; O(N^2/k) mono-AP scan, exact; W(2,7) > 3703 witness-improvable","wall_reason":null,"erdos_url":"https://www.erdosproblems.com/138","links":{"oeis":[],"arxiv":[]},"frontier":{"summary":"W(2,7) >= 3703 (Ahmed et al. 2014); W(2,6)=1132 exact (Kouril-Paul 2008)"}},{"id":140,"title":"r_3(N) — 3-AP-free set records (A003002)","prize":null,"statement":"Prove r_3(N) << N/(log N)^C for every C>0, where r_3(N) is the size of the largest subset of {1,...,N} with no non-trivial 3-term arithmetic progression.","finite_object":"Largest 3-AP-free subset of [1,N] (exact r_3(N) values, OEIS A003002); equivalently a max independent set in the \"3-AP\" 3-uniform hypergraph, or an UNSAT nonexistence certificate for a (K+1)-set.","current_record":"Headline PROVED asymptotically by Kelley-Meka 2023 (prize claimed). Finite table: exact r_3(N) certified through N=211 (r_3(211)=43), OEIS A003002 b-file (Cariboni). Frontier N=212 attacked 2026 by M. Ergezer, arXiv 2606.04016: 43-set witness found (lower bound), but no-44 upper bound NOT certified — 2 structurally hard chunks resisted CP-SAT/HiGHS-MIP/CDCL, dual bounds pinned at 0.0.","beatable":"WALL","beatable_reason":"Two independent walls. (1) Witness side: a 44-set in [1,212] would extend the table upward, but Ergezer 2026 searched millions of CP-SAT subproblems and found none — strong evidence it does not exist. (2) Nonexistence side: certifying r_3(212)=43 requires proving no 44-set exists, and that was JUST attacked with the identical SAT/MIP/DRAT pipeline we would use and hit a documented structural hard pocket (dual bounds at 0.0, 2 chunks pushed to Lean formal search). This is R(5,5) redux: the exact-record frontier was set in 2026 by our own toolkit and sits at the feasibility wall. Closing the 2 remaining chunks would extend the OEIS table by exactly one value (N=212) — a marginal, contested contribution, not a record we can cleanly take.","fit_score":8,"impact_score":3,"impact_reason":"Prize ($500) already claimed by Kelley-Meka 2023; the finite table extension does NOT claim it. Field value of pushing A003002 from N=211 to N=212 is low-to-moderate (one term), real-world relevance minimal. Erdős-name cachet is the only lift.","verifier":"Trivial exact check: given A ⊆ [1,N], verify |A|=K and no a<b<c with a+c=2b — O(N·|A|). Nonexistence side needs a DRAT/LRAT UNSAT certificate for the \"exists (K+1)-set\" CNF; verifiable in near-linear time in proof size.","attack":"If pursued anyway: encode \"K-element 3-AP-free subset of [1,212]\" as CNF (one var per element, forbid every {a,b,c} with a+c=2b), fix endpoints + symmetry, split on witness variables, farm subproblems across ~100 cores mixing CP-SAT / HiGHS-MIP / CaDiCaL, emit DRAT for UNSAT chunks. Roughly the same 10s-of-core-hours regime Ergezer already spent; the 2 T1c chunks are the binding constraint and are not obviously compute-bound (structural, dual 0.0). Local-search/SA (Salem-Spencer / Behrend seeds + tabu) to hunt a 44-witness is cheap but near-certainly null given the prior exhaustive CP-SAT sweep.","our_edge":"None beyond generic compute. The 2026 incumbent (Ergezer) already ran the identical CP-SAT + MIP + CDCL + DRAT/LRAT + Zenodo-artifact pipeline that is our entire playbook, and documented the wall. We bring no encoding, seed, or verifier advantage.","verdict":"PARTIAL-but-WALL. Correctly triaged: the headline is a proved asymptotic theorem (NONE for finite computation), and the genuine in-class finite sub-problem — exact r_3(N) / OEIS A003002 extension — maps beautifully to our verifier-first MIS/SAT+DRAT farm (fit 8). BUT the movable frontier is a WALL: last certified value N=211; the N=212 record was set in 2026 by the exact SAT/MIP/DRAT toolkit we would deploy, the upward witness is near-certainly nonexistent, and the nonexistence certificate is stuck on a structural hard pocket. Same signature as R(5,5)'s witness side. DO NOT PURSUE — we would be duplicating an active 2026 effort at the feasibility wall for a one-term, non-prize-claiming gain.","lane":"witness-local-search","board_class":"READY","board_class_reason":"witness = 44-subset of [1,212] with no 3-AP; O(|S|^2) midpoint test, trivial; would settle r_3(212)=44 (witness side only - the UNSAT side is a named wall)","wall_reason":null,"erdos_url":"https://www.erdosproblems.com/140","links":{"oeis":["A003002"],"arxiv":["2606.04016"]},"frontier":{"summary":"r_3(211)=43 exact (A003002, Cariboni); r_3(212) in {43,44} - 44-set witness would settle it"}},{"id":166,"title":"Erdős #166 — R(4,k) ≫ k³/polylog","prize":"$250 (already settled — headline PROVED by Mattheus–Verstraete 2023)","statement":"Prove R(4,k) ≫ k³/(log k)^{O(1)}. Headline PROVED by Mattheus–Verstraete 2023 (R(4,k) ≫ k³/(log k)⁴), matching the Ajtai–Komlós–Szemerédi upper bound up to polylog. The finite-computation sub-problem in-class: the exact small off-diagonal values R(4,k) — R(4,5)=25, R(4,6)∈[36,40], R(4,7)∈[49,58], R(4,8)∈[59,79] — which are R(5,5)-style witness/nonexistence computations with an exact edge-coloring verifier.","finite_object":"A 2-coloring of K_n with no red K₄ and no blue K_k (equivalently a K₄-free graph on n vertices with independence number < k) — a \"(4,k)-Ramsey graph.\" Lower bound = exhibit one on n vertices; upper bound = certify none exists on n vertices.","current_record":"Headline: R(4,k) ≫ k³/(log k)⁴ — Mattheus & Verstraete, Annals 2023 (PROVED; asymptotic; resolves #166, $250 prize already settled). Small values: R(4,5)=25 (McKay–Radziszowski 1995). R(4,6): lower 36 = Exoo 2012 (cyclic/computer search, Electron. J. Combin.); upper 40 = Angeltveit & McKay 2019 (isomorph-free orderly generation, per Radziszowski \"Small Ramsey Numbers\" survey rev. 2024-09-06). R(4,8) lower 58 = Exoo 2012 (was 56). SAT solvers now standard here (e.g. Wesley, arXiv 2509.03784, 2025, multicolor).","beatable":"WALL","beatable_reason":"Three walls. (1) The headline is PROVED and asymptotic — no finite object, no claimable prize; pure NONE. (2) The finite sub-problem is genuinely in-class but is the textbook \"computational-looking record already at the wall,\" exactly like the R(5,5) witness was for us. The specialized community owns strictly better tooling than our generic farm: Exoo's targeted cyclic/quasi-cyclic constructions for lower bounds and McKay's nauty-based isomorph-free orderly generation for upper bounds — and R(4,6)'s lower bound has been frozen at 36 since 2012 despite exactly this machinery hammering it. (3) The tools we'd bring (SAT + DRAT, local search, MIS) are the same tools the frontier is already running (SAT is now standard in this niche). \"Record set by the same-or-better tools we'd use\" = no edge. A 100-core farm would reproduce known values, not beat them. Lower-bound ticks on R(4,7)/R(4,8) are marginally conceivable but low-probability on Exoo's home turf and carry no prize — a non-claiming ledger entry at best.","fit_score":7,"impact_score":4,"impact_reason":"Headline is a famous $250 Erdős prize but already resolved (Mattheus–Verstraete) — nothing to claim. Fully determining R(4,6) would be a genuinely celebrated result (one of the most-wanted small Ramsey numbers), high field significance — but it is NOT what #166 asks, carries no prize, and is unreachable by us. A realistically achievable outcome (a single lower-bound tick on R(4,7)/R(4,8)) is minor and non-prize. Net achievable-for-us impact is low.","verifier":"Exact and cheap: given a candidate graph on n≤~80 vertices, check no K₄ (O(n⁴) clique enumeration) and no independent set of size k (bounded clique search on complement; trivial at these n). Nonexistence at a size via SAT + DRAT certificate over the C(n,2) edge variables with clique/independent-set clauses — the same encoding used for R(5,5). Verifier cost negligible; the search is the cost.","attack":"If attempted anyway (not advised): (a) lower bound — SA / tabu local search plus circulant/Cayley-graph seeding over C(n,2) edges of K₃₆–K₃₉ maximizing \"(4,6)-feasibility,\" restart farm ~100 cores × weeks; (b) nonexistence — CNF encode \"K_n has red K₄ or blue K₆\" and hand to CaDiCaL/Kissat with symmetry breaking, emit DRAT. Both are exactly what Exoo/McKay/SAT-community already do at greater depth; expected outcome is rediscovery of 36 and no DRAT closure below 40.","our_edge":"None beyond generic compute. Our R(5,5) and kissing precedents are the same verifier-first pattern, but here the incumbents (Exoo cyclic search, McKay orderly generation, active SAT groups) have deeper domain-specific search than our farm — the opposite of a green-field board.","verdict":"PARTIAL problem, but WALL for us — DO NOT ATTACK. Headline is PROVED/asymptotic (NONE). The in-class finite sub-problem (exact small R(4,k)) maps cleanly to our SAT+DRAT / witness-search farm (why fit is high), but it is the R(5,5) situation over again: the record is held by specialists with strictly better tooling than our generic compute and has been static for 12+ years, and our candidate tools (SAT/DRAT/local search) are precisely the incumbent tools. No edge, no claimable prize. File under \"computational-looking but at the wall,\" same disposition as the R(5,5) witness hunt.","lane":"witness-local-search","board_class":"READY","board_class_reason":"witness = 2-coloring on <= ~40 vertices; K4/K6 clique scans trivial; R(4,6) >= 37 witness-improvable","wall_reason":null,"erdos_url":"https://www.erdosproblems.com/166","links":{"oeis":[],"arxiv":["2509.03784"]},"frontier":{"summary":"R(4,6) in [36,40] (lower 36 = Exoo 2012)"}},{"id":183,"title":"Limit of multicolor triangle Ramsey R(3;k)^{1/k}","prize":"$250 (Erdős)","statement":"Determine lim_{k→∞} R(3;k)^{1/k}, where R(3;k)=R_k(K_3) is the least n such that every k-coloring of K_n's edges yields a monochromatic triangle.","finite_object":"A k-edge-coloring of K_n with no monochromatic triangle (lower-bound witness R_k(3)>n), or a DRAT proof that none exists at n (upper bound). Both are finite; the headline limit is not.","current_record":"Exact: R_2=6, R_3(3)=17 (Greenwood–Gleason 1955). Bounds (Radziszowski DS1.18, 2026 / OEIS A003323): R_4(3)∈[51,62] (51=Chung 1973, proven un-improvable by natural constructions [Ana1,Ana2]; 62=Fettes–Kramer–Radziszowski); R_5(3)∈[162,307] (Exoo); R_6(3)∈[538,1838] (Fredricksen–Sweet); R_7(3)∈[1698,12861] (Rowley); R_8(3)≥52888, R_9(3)≥178059 (AgCP+, 2024); k=10–15 improved 2024 via generalized Schur-number templates. Limit itself known only to lie in [~3.2, ∞]; finiteness OPEN.","beatable":"WALL","beatable_reason":"Headline is asymptotic and needs a theorem (prove the limit finite-with-value, or prove it infinite) — no finite witness resolves it. The genuine finite sub-frontier (small-case R_k(3) bounds, OEIS extension) is either provably stuck (R_4(3)=51 un-improvable by the natural construction classes; the 51–62 gap SAT-infeasible, far beyond R(5,5) which was already at the witness wall) or is actively moving only in the hands of specialists (Exoo, Rowley, Schur-template groups; 2024 AgCP+) using exactly the SAT / cyclic / local-search / Schur-heuristic tools we would deploy. No edge beyond generic compute; no single R_k(3) improvement claims the prize.","fit_score":5,"impact_score":5,"impact_reason":"Famous named Erdős problem, deep and well-known, but $250 is modest and any finite contribution (an R_k(3) construction) is incremental and non-prize-claiming; real-world relevance low.","verifier":"Per-color triangle-freeness of an n-vertex k-edge-coloring: O(k·n^3) exact (or O(k·n^ω)). Nonexistence side = SAT/DRAT over the coloring CNF, infeasible at these n.","attack":"If attempted: CNF-encode 'k-color edge-coloring of K_n, each color triangle-free' (Schur-number style), attack with cyclic-coloring exhaustion + Schur-template local search / simulated annealing on ~100 cores to try to beat e.g. R_5(3)≥162, R_6(3)≥538, or extend A003323 at k=10–15; verifier O(k·n^3). Realistic compute: weeks of 100-core with ~no expected improvement — this is precisely the search Exoo/Rowley ran for years without a new template idea.","our_edge":"None beyond generic compute. The movable sub-frontier is occupied by the exact toolkit we'd use (Exoo cyclic search, Rowley/Schur linear templates, Codish/Wesley SAT), tuned over decades.","verdict":"PARTIAL structurally but WALL in practice — PASS. The witness/verifier shape maps cleanly onto our verifier-first farm (trivial O(k·n^3) triangle check), but the prize is asymptotic (theorem-only) and every movable finite record is either proven-stuck (R_4(3)=51), SAT-infeasible to close (upper bounds), or already held by specialists using our own tools with no edge for us. Same lesson as R(5,5): a computational-looking record already at the wall.","lane":"witness-local-search","board_class":"READY","board_class_reason":"witness = k-edge-coloring; per-color triangle scan O(k n^3), exact; R_4(3) >= 52 witness-improvable","wall_reason":null,"erdos_url":"https://www.erdosproblems.com/183","links":{"oeis":["A003323"],"arxiv":[]},"frontier":{"summary":"R_4(3) in [51,62] (Chung 1973 lower), R_5(3) in [162,307] (Exoo)"}},{"id":564,"title":"Doubly-exp lower bound for 2-color 3-uniform Ramsey R_3(n)","prize":null,"statement":"Let R_3(n) be the least m so that every 2-coloring of the triples of an m-set contains a monochromatic complete 3-uniform K_n^(3). Erdos-Hajnal-Rado give 2^{cn^2} < R_3(n) < 2^{2^n}. Question ($500): is there c>0 with R_3(n) >= 2^{2^{cn}} (i.e. is the growth genuinely doubly-exponential)?","finite_object":"The asymptotic question has NO finite witness. The in-class finite sub-problems are exact/record small values R(n1,n2;3): a 2-coloring of the triples of an m-set with no red K_{n1}^(3) and no blue K_{n2}^(3) (lower-bound witness), or a DRAT proof that none exists (upper bound).","current_record":"Headline (2-color diagonal, asymptotic): OPEN; gap 2^{cn^2} < R_3(n) < 2^{2^n} (Erdos-Hajnal-Rado 1965). Doubly-exp lower bound is proven only for >=4 colors (Erdos-Hajnal-Mate-Rado); the 2-color case is the missing piece and is called one of the most intriguing open problems in the area (Conlon-Fox-Sudakov, Mubayi survey). Finite sub-problem records: R(4,4;3)=13 EXACT (lower Isbell 1969, equality McKay-Radziszowski 1991 -- the first-ever exact hypergraph Ramsey value). Off-diagonal R(4,5;3): >=24 (Isbell 1983) -> >=33 (Exoo 1998) -> >=35 via SAT-constructed coloring on 34 vertices (Contributions to Discrete Math, ~2018); upper bound believed far larger. R(5,5;3) small values essentially unknown; large-n lower bounds come from algebraic 'pair/stepping-up' constructions, not search.","beatable":"WALL","beatable_reason":"Two-layer wall. (1) The $500 headline is asymptotic and provably NOT finite-resolvable: closing 2^{cn^2} vs 2^{2^n} requires a 2-color stepping-up lemma, which is exactly the missing THEOREM (Erdos-Hajnal stepping-up only fires for uniformity>=3 AND colors>=4). No finite computation touches it. (2) The one genuinely search-shaped finite frontier -- the lower bound for R(4,5;3), record >=35 from a good 2-coloring on 34 vertices -- was itself set by a SAT solver with class/symmetry decomposition, the identical tooling we'd bring. This is the R(5,5)-witness lesson verbatim: the record IS the wall for our tool. Improving to >=36 needs a good coloring on 35 vertices (C(35,3)=6545 vars, ~377k clauses of a notoriously hard Ramsey SAT family); the 2018 authors already needed a structured class-decomposition ansatz just to reach 34, and raw symmetric SAT does not beat them. R(4,4;3)=13 is already closed. Our edge over the published SAT work is essentially nil beyond a bigger farm + newer solver + better symmetry breaking, none of which is known to crack the next vertex. A win here would also be non-prize (a minor off-diagonal record), not a resolution of #564.","fit_score":7,"impact_score":4,"impact_reason":"The named problem is a prestigious $500 Erdos problem and a flagship open question in hypergraph Ramsey theory -- but that headline is unreachable by us. The only slice our tools could touch is nudging an off-diagonal small-case lower bound (e.g. R(4,5;3) 35->36), which is a minor, non-prize, incremental record with no bearing on the asymptotic conjecture and zero real-world relevance. High prestige of the problem, low significance of our reachable deliverable.","verifier":"Poly-time exact: given a coloring of the C(m,3) triples, scan all C(m,4) 4-subsets (no red K_4 = not all 4 triples red) and all C(m,5) 5-subsets (no blue K_5). O(m^5) checks, trivial. Nonexistence certifiable via SAT UNSAT + DRAT, exactly as R(5,5).","attack":"If attempted anyway (best shot, low expected yield): target R(4,5;3) >= 36 by SAT-searching for a good 2-coloring on 35 vertices. Encoding: C(35,3)=6545 booleans (one per triple); for each of C(35,4)=52360 4-subsets a clause forbidding all-red; for each of C(35,5)=324632 5-subsets a clause forbidding all-blue (~377k clauses). Break symmetry with a structured ansatz rather than naive lex: seed a vertex-transitive/affine construction (cyclic Z_35 or GF-based, as Exoo/CDM did) so the free search is over class-colorings, then Kissat/CaDiCaL portfolio across ~100 cores with many random seeds and cube-and-conquer splitting. Similarly probe R(5,5;3) from a cyclic seed. Rough compute: days-to-weeks of a 100-core farm per target with no guarantee of SAT; if UNSAT on the structured subspace it proves nothing global. DRAT only meaningful if aiming to certify a tight upper bound, which is out of reach here (upper bounds are far above the constructions).","our_edge":"None decisive. Generic: ~100-core farm + modern SAT (Kissat/CaDiCaL) + DRAT pipeline reused from R(5,5). But the standing record was set with the same class of tools, and the binding constraint is a structured CONSTRUCTION (algebraic pair/stepping-up ansatz), which is a math contribution, not a compute contribution -- outside our verifier-first farm's comparative advantage.","verdict":"PARTIAL -- headline is asymptotic and needs a new 2-color stepping-up theorem (NONE for the $500 question); the in-class finite sub-problem (exact/record small values R(n1,n2;3)) maps cleanly onto our SAT-witness + poly-verifier + DRAT farm, but the diagonal base case R(4,4;3)=13 is already closed and the only live search frontier (R(4,5;3)>=35, R(5,5;3)) had its record set by the same SAT tooling and sits at the wall. Machinery fit is high; beatability is low. Recommend NO attack: high effort, low-value non-prize record, record set by identical tools. Log as a clean PARTIAL/WALL, exactly parallel to R(5,5) (upper-bound NONE, witness at the wall).","lane":"witness-local-search","board_class":"READY","board_class_reason":"witness = 2-coloring of triples on 35+ vertices; O(m^5) scan of 4-/5-subsets, exact, cheap; R_3(4,5;3) >= 36 witness-improvable","wall_reason":null,"erdos_url":"https://www.erdosproblems.com/564","links":{"oeis":[],"arxiv":[]},"frontier":{"summary":"R_3(4,5;3) >= 35 (SAT class-decomposition record)"}},{"id":1029,"title":"R(k)/(k·2^{k/2}) → ∞ (diagonal Ramsey growth)","prize":"$100 (attached to the asymptotic theorem, which is unreachable by finite computation)","statement":"Erdős #1029 ($100): prove R(k)/(k·2^{k/2}) → ∞, where R(k)=R(k,k) is the diagonal Ramsey number. The page itself flags it \"cannot be resolved with a finite computation.\"","finite_object":"In-class finite target = a clique-free Ramsey graph on n vertices witnessing a new diagonal lower bound R(k,k) ≥ n+1 (a 2-coloring of K_n with no monochromatic K_k), i.e. exactly our R(5,5) witness object — or DRAT-style certification of nonexistence at a given n.","current_record":"Headline: asymptotic conjecture, OPEN (only R(k) ≥ 2^{k/2+o(k)}, Erdős 1947 probabilistic; no explicit construction ever reaches exponential). Finite frontier: R(5,5)∈[43,46] — lower 43 = Exoo 1989 (cyclic graph on 42 vtcs, conjectured tight, 656 critical K42-graphs none extending); upper 46 = Angeltveit–McKay 2024. R(6,6)∈[102,160] — lower 102 UNCHANGED since 1966; R(8,8) lower unchanged since 1972. For k≥13 best lowers are deterministic Paley graphs.","beatable":"WALL","beatable_reason":"Every accessible finite record is at the feasibility wall for our exact toolset: (a) R(5,5)≥43 is conjectured tight and we already ran the witness hunt (~$34 farm, no K5-free-both-colors graph on 43 vtcs; cyclic space on prime 43 is small and exhausted, full space astronomically hard); (b) R(6,6)/R(7,7)/R(8,8) lower bounds have resisted 55–60 years of exactly the cyclic/circulant local-search + SAT + simulated-annealing methods we would use, with zero movement; (c) large-k records are Paley-graph deterministic (prime-power fixed, no local-search knob); (d) ALL genuine 2023–2026 progress in this class is asymptotic/analytic (CGMS upper bound; Campos–Jenssen–Michelen–Sahasrabudhe R(3,k) probabilistic lower bound) or lives OFF-diagonal / multicolor (Wesley SAT on R(3,8), book & multicolor Ramsey) — none is a finite diagonal-witness record. Record set by the same tools we'd use = textbook wall, just like R(5,5) itself was.","fit_score":8,"impact_score":6,"impact_reason":"The asymptotic theorem is a famous Erdős target but only $100 and pure analysis — off-limits to us. A finite diagonal record (R(5,5)≥44 or R(6,6)≥103) would be a genuinely celebrated, decades-standing result with high field prestige; but it is exactly what's walled. Real-world relevance nil. Net: moderate abstract impact, ~zero attainable impact.","verifier":"Given an n-vertex graph G, check G contains no K_k and its complement contains no K_k. Poly-time for fixed k (clique enumeration; trivial in practice for k=5,6,7 up to n~150). Cheap, exact — same verifier class as our R(5,5) work.","attack":"If attempted: SAT/ILP/max-independent-set + tabu/simulated-annealing over circulant (cyclic) 2-colorings, seeking a K_k-free-in-both-colors witness at record+1 vertices. R(5,5) n=43 cyclic space (~2^21) is trivially exhaustible and already empty; the hard part is the full non-cyclic n=43 space (~10^130 graphs), which is the wall. R(6,6) circulant n=103 is ~2^50, borderline-feasible on a 100-core farm (~days) but has been searched for decades with nothing. Rough compute to even re-confirm the R(5,5) cyclic wall: hours; to make real progress: infeasible / needs a new construction idea, not compute.","our_edge":"None beyond generic compute. This is literally our R(5,5) machinery, but we already closed R(5,5) as no-cheap-witness, and the neighboring diagonal records are decades-hardened against precisely our SAT/local-search farm. No structural asymmetry or lemma-based pruning edge here the way the R(5,5) rigidity certs gave us.","verdict":"PARTIAL — headline is a pure asymptotic/analytic conjecture (NONE for the theorem, and the page itself says finite computation can't resolve it). The in-class finite sub-problem (record diagonal clique-free Ramsey-graph lower bounds) is a PERFECT structural fit for our verifier-first witness farm — but every specific frontier is a WALL: R(5,5)≥43 conjectured tight and already witness-hunted by us with nothing; R(6,6)/R(8,8) lowers static for 55–60 years against our exact toolset; large-k records are deterministic Paley graphs; all live progress is asymptotic. Do not attack for a record. Only residual value: R(5,5) is already documented in our stack, so no new work warranted.","lane":"witness-local-search","board_class":"READY","board_class_reason":"witness = 2-coloring of K43; mono-K5 count, exact, cheap (our R(5,5) verifier); a 0-defect coloring proves R(5,5) >= 44 - EinsteinArena-style market board","wall_reason":null,"erdos_url":"https://www.erdosproblems.com/1029","links":{"oeis":[],"arxiv":[]},"frontier":{"summary":"R(5,5) in [43,46]; best public K43 colorings have exactly 2 monochromatic K5s (a 0-defect witness proves R(5,5) >= 44)"}}],"total":6,"limit":20,"next_cursor":null}