{"id":"71265118-2110-4cad-bb07-90f3ff458b4d","arxiv_id":"2607.02958","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":2,"one_line_summary":"The largest set of points in the plane with no empty convex hexagon and no convex heptagon has size 23, proved by a SAT-modulo-realizability solver that finds thousands of witnessing configurations.","lead":"A new SAT-based method finds realizable point sets in the plane and proves that 23 is the largest size avoiding empty convex hexagons and convex heptagons. This shows how to make computer search practical for geometric problems that sit beyond NP.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The paper's strongest claim is an existence statement witnessed by a fully explicit, small-integer point set. Verification of that set requires only elementary orientation predicates and does not depend on the correctness or frequency of Localizer under the flippability heuristic. The reader's identification of the flippability frequency as the weakest assumption is accurate for the broader methodology and for scaling, but it is not load-bearing for the concrete theorem once the witness is in hand. The upper bound is external and already published. Consequently the ACCEPT verdict stands; no adjustment is warranted. The suggested concrete test simply reconfirms the published witness by the most direct means.","tokens_in":15342,"tokens_out":385,"duration_ms":3733,"concrete_test":"Independently recompute all triple orientations of the 23 integer points listed in Figure 1 and confirm that the resulting order type contains neither a 6-hole nor a 7-gon; if the check passes, the existence half of Theorem 1 is settled regardless of any heuristic.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim (Theorem 1) rests on an explicit integer-coordinate 23-point set (Figure 1) that can be checked independently of Localizer, flippability, diversity sampling, or any stochastic component of PointSAT. The matching upper bound of 24 is already established by Heule & Scheucher. The reader's weakest_assumption correctly flags an empirical frequency that is essential for the pipeline's ability to discover constructions, but that frequency is not load-bearing for the existence claim itself once a concrete witness has been published and can be verified by direct orientation computation. Ablations (Table 1) and recovery of known constructions further support the method, yet none of them is required to accept the settled value of h(6,7).","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper introduces PointSAT, a SAT-based framework (satisfiability modulo realizability) for finding realizable point configurations in the plane that satisfy combinatorial constraints expressible via abstract order types. It encodes an underapproximation of the geometric problem as a SAT instance over orientation variables, then uses diversity-driven sampling of abstract solutions (via clause scrambling), partial-realization feedback from the Localizer local-search tool, and a novel flippability heuristic that drops orientation constraints corresponding to flippable variables before calling Localizer. The method is applied to variants of the Erdős–Szekeres happy-ending problem; the central result is Theorem 1, which states that the largest set of points in general position with no 6-hole and no 7-gon has size 23 (hence h(6,7)=24), witnessed by an explicit integer-coordinate configuration of 23 points (Figure 1) together with more than a thousand additional realizations. Supporting experiments recover known constructions (26 points with no 5-cap or 7-gon; 29 points with no 6-hole) and include ablations (Table 1) and statistics on flippable orientations and violation counts.","tokens_in":15526,"tokens_out":785,"duration_ms":13261,"significance":"If the explicit 23-point witness is correct (which can be verified independently by computing orientations), the paper settles the last nontrivial case of h(k,ℓ) for k≤6, closing an open question left by Heule & Scheucher. Beyond the concrete theorem, the work supplies a reusable, publicly available pipeline that systematically searches for realizable order types on problems whose naïve SAT encodings produce overwhelmingly unrealizable abstract solutions. The three heuristics—especially the empirically motivated flippability omission—are shown by ablation to be essential for obtaining any solutions, and the same pipeline recovers previously known constructions without problem-specific algorithms. This constitutes a genuine advance in computer-assisted discrete geometry for ∃ℝ-complete problems and demonstrates that SMT-style interfacing can resolve open existence questions in pure mathematics.","major_comments":[],"minor_comments":[{"comment":"Section 4.2 heading contains a typographical space (“T esting”); similar minor OCR/spacing artifacts appear elsewhere and should be cleaned.","section":null},{"comment":"Figure 3 and Figures 4–7 would benefit from explicit axis labels and a short caption note clarifying that the top-percentile outliers have already been removed (as stated in the footnote).","section":null},{"comment":"The description of how flippable variables are identified (Section 4.3) is clear, but a one-sentence remark on the computational cost of the flip checks (relative to the subsequent Localizer calls) would help readers gauge practicality for larger n.","section":null},{"comment":"Table 2 lists many hull-layer signatures; a brief remark on whether any of the rare signatures that appear only among abstract solutions (never among realized ones) can be ruled out a priori would strengthen the discussion of Theorem 2.","section":null},{"comment":"The integer-grid post-processing pipeline that produced Figure 1 is described only at a high level; a short pseudocode or reference to the annealing scripts would improve reproducibility of the “pretty” drawing.","section":null}],"recommendation":"accept","confidential_remarks":"The central existence claim rests on a publicly listed integer point set that any reader can verify by direct orientation computation; the matching upper bound is already peer-reviewed. The methodological contribution is solid and the ablations are convincing. I see no load-bearing technical flaw. The paper is a natural fit for a computational-geometry or automated-reasoning venue."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The headline result is solid: an explicit integer-coordinate 23-point set with no 6-hole or 7-gon (Figure 1), so together with Heule–Scheucher’s upper bound of 24 we now know h(6,7)=24. That witness can be checked by anyone with a few lines of orientation code; nothing about Localizer, flippability, or supercomputer sampling is load-bearing for the existence claim itself.\n\nWhat is actually new is the search architecture they call “satisfiability modulo realizability.” They encode the combinatorial under-approximation as a SAT instance over abstract order types, then feed candidates to Localizer. The three heuristics—diversity via clause scrambling, checking partial realizations for accidental solutions, and especially the flippability filter that drops orientations that can be flipped while remaining SAT-satisfying—are what make the pipeline find anything at all. Table 1 is clean: without both partial-realization checking and flippability omission they get zero solutions; with both they get hundreds. They also recover known constructions for 26-point no-5-cap/7-gon and 29-point no-6-hole instances, so the method is not a one-off for this particular Ramsey number.\n\nSoft spots are real but secondary. The flippability frequency is purely empirical; if it collapses for larger n the pipeline stalls even when constructions exist (they already fail to find a 32-point no-7-gon). Localizer remains a black-box stochastic local searcher, and the bulk of the 23-point solutions required thousands of core-hours. None of that touches the published witness or the settled value of h(6,7). Citations look standard; self-cites to Localizer and the prior upper bound are appropriate.\n\nThis is for people who care about computer-assisted discrete geometry or about making ∃R existence questions tractable via SAT. It deserves a serious referee. I would accept it for peer review and would cite the construction and the flippability idea.","headline":"They settle h(6,7)=24 with an explicit 23-point integer witness and a reusable SAT+Localizer pipeline whose flippability heuristic is the real novelty.","tokens_in":16131,"tokens_out":504,"would_cite":true,"duration_ms":4633,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["52C10","68Q17"],"pacs":[],"model":"grok-4.5","headline":"The largest set of points with no empty convex hexagon and no convex heptagon has size exactly 23.","keywords":["discrete geometry","SAT solving","order types","realizability","happy ending problem","existential theory of the reals","PointSAT","flippability"],"falsifier":"Independent verification that the published 23-point integer configuration actually contains a 6-hole or a 7-gon, or discovery of any 24-point set that avoids both.","tokens_in":16240,"feed_emoji":"📐","tokens_out":820,"duration_ms":15275,"temperature":0.7,"pith_summary":"Many problems in discrete geometry are complete for the existential theory of the reals, so exact encodings are hard for SAT. This paper introduces satisfiability modulo realizability: encode an under-approximation of the geometry as a SAT problem over abstract order types, then guide a search toward the rare realizable ones. Diversity sampling, feedback from partial realizations, and a flippability heuristic (omitting orientation variables that can flip while remaining abstractly feasible) make the search succeed where naive enumeration fails. The method settles an open case of the happy-ending problem by constructing thousands of 23-point sets with neither a 6-hole nor a 7-gon, matching a prior upper bound of 24. A reader cares because the same pipeline recovers known constructions for related problems without any problem-specific geometric code, showing a practical route for computer-assisted discovery beyond pure SAT.","feed_headline":"Largest set avoiding 6-holes and 7-gons has size 23","feed_subtitle":"SAT plus local search constructs the missing point set that settles the open bound","key_machinery":"Satisfiability modulo realizability (PointSAT): SAT encoding of geometric constraints over abstract order types, diversity-driven generation of abstract solutions, omission of flippable orientation constraints, and Localizer search for (partial) realizations that are then re-checked for combinatorial validity.","core_discovery":"The largest point set in the plane in general position that contains neither an empty convex hexagon nor a convex heptagon has size 23 (hence h(6,7)=24). The claim is witnessed by an explicit integer-coordinate configuration of 23 points and by more than a thousand additional realizations produced by the PointSAT solver; the matching upper bound of 24 was already known.","pith_inferences":["The flippability observation may transfer to other combinatorial configuration spaces that admit SAT under-approximations.","Hybrid SAT-plus-local-search pipelines of this form could be tried on further open existential-theory-of-the-reals problems whose combinatorial skeletons encode cleanly.","The scarcity of flippable orientations on larger instances (e.g., 32 points) already signals a scaling barrier that future heuristics will need to address."],"forward_implications":["h(6,7) is settled at 24 with an explicit construction of size 23.","The same pipeline recovers known constructions for 26 points without 5-caps or 7-gons and for 29 points without 6-holes, without specialized geometric primitives.","Many orientation constraints in these geometric solutions are non-critical and can be safely omitted during realization search.","Generating many diverse realizations becomes practical, enabling selection of visually clean integer embeddings."],"fun_headline_variants":["SAT finds 23-point set free of empty hexagons and heptagons","Largest plane set without 6-holes or 7-gons has size 23","Order-type SAT settles open problem: 23 points avoid 6- and 7-gons","PointSAT builds 23-point configuration missing empty 6-gons and 7-gons","Realizable abstract order types prove h(6,7)=24 via size-23 witness"],"cache_read_input_tokens":128,"weakest_assumption_plain":"Dropping the flippable orientations and accepting imperfect partial realizations still produces combinatorially valid geometric solutions often enough for the search to succeed.","fun_headline_variants_meta":{"raw":{"variants":["SAT finds 23-point set free of empty hexagons and heptagons","Largest plane set without 6-holes or 7-gons has size 23","Order-type SAT settles open problem: 23 points avoid 6- and 7-gons","PointSAT builds 23-point configuration missing empty 6-gons and 7-gons","Realizable abstract order types prove h(6,7)=24 via size-23 witness"]},"model":"grok-4.5","effort":"low","cost_usd":0.003946,"raw_usage":{"total_tokens":1179,"prompt_tokens":686,"num_sources_used":0,"completion_tokens":123,"cost_in_usd_ticks":39460000,"prompt_tokens_details":{"text_tokens":686,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":370,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":686,"tokens_out":123,"duration_ms":3108,"temperature":1.0,"reasoning_tokens":370,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-12T05:49:28.356324+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Independent verification that the published 23-point integer configuration actually contains a 6-hole or a 7-gon, or discovery of any 24-point set that avoids both.","supporting_citations":[],"review_version":1}