{"id":"8f500ff5-717e-46b9-8232-b8406ad99d45","arxiv_id":"2507.07951","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":3,"one_line_summary":"New computational constructions claim to achieve the upper bounds for 23 and 27 lines in the Kobon triangle problem, yielding N(23)=161 and N(27)=225, subject to the reliability of a heuristic straightening step.","lead":"This paper presents new computer tools for the Kobon triangle problem, a geometry puzzle asking for the largest number of non-overlapping triangles that n straight lines can form. The author reports new constructions for 23 and 27 lines reaching the theoretical upper bounds, fixing N(23)=161 and N(27)=225, along with a table notation and SAT-based search.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The proof hinges on heuristic straightening (Sec. 4.4): a numerical optimizer drives a target function near zero, and for n=27 a hand-tuned coefficient is needed. Without exact coordinates or a stretchability certificate, the Appendix C tables do not prove N(23)=161 and N(27)=225.","rationale":"The strongest claim is genuinely about proving exact values N(23)=161 and N(27)=225. The paper's pipeline is reasonable and has independent support: the tools reproduce many previously known optimal arrangements, and the SAT encoding plus heuristic straightening is a plausible discovery method. However, the proof of the new values requires that the tables in Appendix C are realized by actual straight lines. The paper's own Section 4.4 says that even nonzero minimization values 'often correspond to perfectly acceptable solutions', which is fine for heuristic discovery but not for a proof. For n=27, the additional hand-picked coefficient in Table 1 makes the straightening step even more fragile. The tables alone are pseudoline order data; stretchability is a real, nontrivial condition, and the paper gives no exact coordinates or certificate. This is precisely the reader's weakest assumption, and it is load-bearing because the upper bound n(n-2)/3 is only attained by a genuine straight-line arrangement. I therefore agree with the CONDITIONAL verdict: the results are plausible and worth pursuing, but the proof should be completed by supplying exact/certified realizations or a machine-checked stretchability witness. This is not a rejection of the work; it is a request for the missing certificate that the word 'proving' requires.","tokens_in":17702,"tokens_out":4278,"duration_ms":51986,"concrete_test":"Take the 23-line table in Appendix C.5 and verify stretchability in exact arithmetic: convert the table to a rank-3 oriented matroid (or directly to the ordering inequalities F(i,j,k)<0 from Section 4.1) and run an exact realizability check — e.g., compute a rational point with Cylindrical Algebraic Decomposition after half-angle substitution, or solve the resulting polynomial feasibility problem with Mathematica/Maple — then check the reported 161 triangle count from the exact realization. Repeat for n=27. If no exact realization exists, the central proof claims fail.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Section 3.3 and Appendix C assert 'proving N(23)=161 and N(27)=225'. The only bridge from combinatorial tables to straight-line arrangements is the SciPy minimization in Section 4.4; Section 4.4 explicitly accepts nonzero target values as 'perfectly acceptable solutions', and Table 1 records that n=27 requires a hand-chosen main coefficient (0.5). The tables are order data for pseudolines, and not every pseudoline arrangement is stretchable (realizability of rank-3 oriented matroids is already nontrivial, cf. [6]). If the minimized configuration merely approximates the table's order, it may not realize all 161/225 triangles exactly: small violations can create overlaps or alter the triangle count. The paper supplies no exact coordinates, rational rounding, or error certificate for n=23 or n=27. Since equality N(n)=n(n-2)/3 follows only from an actual straight-line arrangement attaining the upper bound, the claim is not yet proven; it is a strong computational conjecture requiring certification.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a compact table notation for encoding pseudoline arrangements and a SAT-based CNF model for searching optimal Kobon triangle arrangements, together with a heuristic straightening method based on numerical optimization. The authors report new optimal arrangements for 23 and 27 lines, claiming that these establish N(23)=161 and N(27)=225, and they also report the absence of a 33-triangle arrangement for 11 lines, along with several other computational results. The tools are released as open-source repositories, and the paper includes reproduction of many previously known optimal arrangements as a sanity check.","tokens_in":18020,"tokens_out":7036,"duration_ms":66263,"significance":"If the 23- and 27-line claims are correct, the paper settles two open instances of the Kobon triangle problem and demonstrates a potentially powerful computational pipeline combining pseudoline table encodings, SAT solving, and numerical straightening. The reproduction of known optimal arrangements and the n=11 negative result are useful validations of the framework. However, the claimed proofs currently depend on a heuristic optimization step that does not provide exact coordinates or certificates, and the CNF-to-table equivalence is asserted rather than rigorously established. The framework is promising, but the central claims are not yet backed by complete mathematical evidence.","major_comments":[{"comment":"The claimed proofs of N(23)=161 and N(27)=225 require an actual straight-line arrangement attaining the upper bound, but the bridge from the Appendix C tables to straight lines is a heuristic numerical optimization that explicitly accepts nonzero target-function values, and for n=27 it requires a hand-chosen coefficient (0.5, Table 1 footnote). Since the Appendix C tables are only order data for pseudolines and not every pseudoline arrangement is stretchable, the existence of the required straight-line arrangements is not established. Please provide exact coordinates (or a rigorous stretchability certificate, e.g., rational coordinates verified by exact arithmetic) for the 23- and 27-line arrangements, and a programmatic check that all 161/225 triangles are bounded and non-overlapping. Without this, the statements 'proving N(23)=161' and 'proving N(27)=225' in Section 3.3 and Appendix C should be weakened to computational evidence.","section":"Section 4.4 and Table 1"},{"comment":"The soundness and completeness of the CNF encoding are asserted without proof. Rule 12 is described as enforcing 'Consistency + Optimality' by using the same clauses for G and X, but no theorem states that a satisfying assignment corresponds exactly to a table of an optimal Kobon arrangement, including the handling of parallel lines and multiple-intersection points. This is load-bearing for all SAT-based results, including the n=11 unsat conclusion in Section 5 ('cannot be built even with pseudolines') and the enumeration claims for n in {3,5,9,15,17}. Please provide a precise formal statement and proof, or at least a rigorous argument, that the clause set is satisfiable if and only if a valid optimal table exists for the specified n values.","section":"Section 3.2, Rule 12"},{"comment":"For n=23, Table 1 records the search as non-exhaustive ('≥ 65', '≥ 6', footnote d), which is acceptable for an existence proof, but the paper's broader enumeration claims need careful scoping. In the Conclusion, the statement 'for n ∈ {3,5,9,15,17} we enumerate all possible Kobon arrangements' is ambiguous: it must specify what 'possible' means (all missing-triangle multisets? all symmetry classes? all tables satisfying the CNF model?) and must be conditional on the CNF model's completeness. Without this, the enumeration claim is unsupported. Please specify the exact scope of each exhaustive search and the configurations covered.","section":"Section 3.3 and Conclusion"}],"minor_comments":[{"comment":"In the definition of variable X(r,i,j), the text says 'line j is somewhere after line j'; this should read 'line j is somewhere after line i'.","section":"Section 3.1"},{"comment":"The table construction for multiple-line intersections is under-specified: clarify how groups are ordered when more than three lines meet at a single point, and explain how parallel lines are handled in the CNF model in Section 3.","section":"Section 2.1"},{"comment":"Table 1 is very hard to parse: the columns for -M, -R, -L, tabs, fit, and the various timing columns are not cleanly aligned, and the footnote markers are ambiguous. Please reformat the table with separate flag columns and numeric count columns, and ensure each row is legible.","section":"Table 1"},{"comment":"The statement that 'nonzero values often correspond to perfectly acceptable solutions' needs a precise fail criterion; state the tolerance used and how the final arrangement is validated (for example, by recomputing the triangle count with a separate routine and by checking that all ordering constraints are satisfied).","section":"Section 4.4"},{"comment":"The arrangements in Appendix A are given as decimal approximations and symbolic epsilon values; since these are claimed to be straight-line realizations, provide exact rational expressions for the coefficients or state clearly that they are numerical approximations only.","section":"Appendix A"},{"comment":"Reference [1] is incomplete: it lists only 'Handbook of discrete and computational geometry. chapter 5, page 126' without authors, editors, or title; please complete the citation.","section":"References"},{"comment":"The abstract mentions 'several other new results' without specifying them; please enumerate these results explicitly in the Conclusion (for example, the 24-line 172-triangle arrangement and the 22- and 28-line variants mentioned in Section C.2).","section":"Abstract and Conclusion"}],"recommendation":"major_revision","confidential_remarks":"The paper presents a genuinely interesting computational framework and the n=23/n=27 results, if certified, would be valuable. The main concern is that the proof claims in the abstract and Section 3.3 outrun the evidence: the straightening step is heuristic and no exact coordinates are supplied, and the CNF model's equivalence is stated without proof. These issues are fixable in revision by adding certificates and formal arguments, or by weakening the claims to conjectures. The paper's reliance on GitHub repositories for the main tools is acceptable given the current practice in computational mathematics, but the manuscript should clearly state the versions and commit hashes used for reproducibility."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The short version: the pipeline is real, the results are likely real, but the word \"proving\" in the abstract is doing heavy lifting it isn't rated for. This is a computational paper that finds new Kobon arrangements for 23 and 27 lines and reports an 11-line unsat result. The table notation is compact and genuinely useful, the SAT encoding with Kissat is a sensible way to search pseudoline orders, and the straightening heuristic recovers many known optimal arrangements, which is a good sanity check. The tools are on GitHub and the candidate tables are printed in the appendix, so the work is reproducible.\n\nThe soft spot is exactly where the stress-test lands. The bridge from table to straight-line arrangement is a SciPy minimization (Section 4.4) that accepts nonzero target values as \"perfectly acceptable solutions,\" and for n=27 the success depends on a hand-chosen coefficient. No exact coordinates or stretchability certificates are given for the 23- and 27-line cases. Since not every pseudoline arrangement is stretchable, the tables in Appendix C do not, by themselves, prove N(23)=161 or N(27)=225. The CNF consistency clauses in rule 12 are asserted without a proof that they exactly capture the Kobon-optimal pseudoline condition; that is fixable but currently missing. The n=11 unsat claim also lacks a SAT unsat certificate, so it is not independently verifiable from the paper.\n\nNone of these are fatal to the paper's value as a computational contribution. They are fatal to the paper's current proof language. The fix is straightforward: supply exact rational coordinates (or a formal stretchability certificate) for the 23/27 arrangements, verify the triangle count against those coordinates, provide a proof or machine-checked validation of the encoding, and include an unsat certificate for n=11 or clearly label it as a computational negative result.\n\nI'd send this to a serious referee—the subfield will care about the new constructions and the tools—but with the expectation of major revisions. The claims need to be scaled back to \"computational evidence\" until the certificates appear, or the certificates need to be added.","headline":"Solid computational pipeline, but the claimed proofs for n=23 and 27 rest on heuristic straightening with no exact certificates, so treat the headline results as strong conjectures.","tokens_in":18477,"tokens_out":2807,"would_cite":true,"duration_ms":33396,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["52C30"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper reports new optimal Kobon triangle arrangements for 23 and 27 lines, reaching the known upper bounds of 161 and 225 triangles.","keywords":["Kobon triangles","line arrangements","pseudoline arrangements","SAT encoding","combinatorial tables","heuristic straightening","upper bounds","computational geometry"],"falsifier":"Run an independent exact-arithmetic check on the Appendix C tables for 23 and 27 lines: attempt to solve for line angles and offsets so that every prescribed crossing order and triangle-side condition holds with zero violation, or produce a realizability certificate for those tables. If no such exact configuration exists, or if a consistency contradiction is found between the table and the geometry of straight lines, the central claims N(23) = 161 and N(27) = 225 are false.","tokens_in":17492,"feed_emoji":"📐","tokens_out":6327,"duration_ms":69132,"temperature":0.7,"pith_summary":"The paper takes on the Kobon triangle problem, which asks for the largest number of non-overlapping triangles that n straight lines can form. It introduces a compact table notation for pseudoline arrangements, turns the search for optimal tables into a satisfiability (SAT) problem, and then numerically straightens candidate tables into genuine straight-line arrangements. Its headline results are new optimal arrangements for 23 and 27 lines, which meet the known upper bound N(n) = n(n−2)/3 and therefore give N(23) = 161 and N(27) = 225. The same machinery also exhaustively settles several small cases and shows that no pseudoline arrangement with the optimal 33 triangles exists for 11 lines.","feed_headline":"Two new Kobon records: 161 and 225","feed_subtitle":"Automated table search and SAT solving reach the known upper bounds for 23 and 27 lines.","key_machinery":"The load-bearing object is the table: a row for each line listing, in order, the other lines that cross it, with groups for multi-line intersections. The table is a combinatorial description of a pseudoline arrangement and supports symmetries and parallel lines. The argument runs through three mechanisms: a CNF encoding with variables expressing which line occupies which column of a row, which line immediately follows another, and which line lies somewhere after another, plus clauses enforcing consistency and optimality; a SAT solver that finds satisfying assignments, i.e., candidate optimal tables; and a heuristic straightening step that represents each line by an angle and a signed distance and minimizes a sum of squared violations so that the prescribed intersection orders hold. The last step is where the combinatorial candidate becomes a concrete arrangement of straight lines.","core_discovery":"The central claim, stated on the paper's own terms, is that the search for optimal Kobon arrangements can be fully automated and that this automation yields new extremal configurations. For line counts n with n mod 6 ∈ {3, 5}, an arrangement attaining the upper bound must use every finite non-overlapping segment as the side of some triangle, which lets the author encode optimality directly as ordering constraints in CNF. A SAT solver applied to those constraints produces candidate tables, and a constrained numerical minimization over line angles and signed distances recovers straight-line drawings. The outcome is a table for 23 lines realizing 161 triangles and two tables for 27 lines realizing 225 triangles, matching the upper bound in each case, together with complete enumeration for n = 3, 5, 9, 15, 17 and a nonexistence result for the 11-line optimum.","pith_inferences":["If the table-and-SAT pipeline were extended to other residue classes by systematically adding missing-triangle variables, the same machinery could test whether other known upper bounds are sharp for small even n and for other congruence classes of n.","Because the straightening step is heuristic, a numerically fitted table is evidence rather than proof; replacing it with exact algebraic verification or a realizability certificate would turn these constructions into fully verified theorems.","The table notation is close to an order-type encoding, so linking table realizability to oriented-matroid theory could let the SAT search exclude unstraightenable pseudoline arrangements at the combinatorial stage."],"forward_implications":["If the 23- and 27-line constructions are accepted, N(23) = 161 and N(27) = 225, both equal to the upper bound n(n−2)/3, so no arrangement with more triangles can exist for those counts.","The 24-line arrangement with 172 triangles, built by inserting a line into the 23-line solution, provides a new benchmark for even n and suggests similar insertions from other odd solutions.","The SAT-based search can certify nonexistence: for 11 lines no pseudoline table with 33 triangles exists, so the optimal 33-triangle configuration cannot be realized even before straightening.","Because the same pipeline reproduces previously known optimal arrangements and can enforce mirror or rotational symmetry, it gives a transferable method for attacking larger n."],"supporting_citations":[{"why":"Supplies the upper bound N(n) ≤ n(n−2)/3 for the residue classes that the new 23- and 27-line tables attain.","marker":"[5]"},{"why":"Gives the combinatorial setting of simple arrangements with the maximum number of triangles and the normal form used for the special arrangements.","marker":"[3]"},{"why":"The SAT solver that finds satisfying assignments for the generated CNF table problems.","marker":"[4]"},{"why":"The accompanying CNF generator that encodes optimal Kobon arrangements and produces candidate tables.","marker":"[15]"},{"why":"The accompanying straightening tool that recovers straight-line arrangements from table candidates, including the new 23- and 27-line results.","marker":"[14]"},{"why":"The sequence entry that records previously known Kobon values which the paper extends.","marker":"[10]"},{"why":"Provides the 16-line example used to construct the even 24-line arrangement by inserting an additional line.","marker":"[2]"}],"fun_headline_variants":["SAT and heuristics yield optimal Kobon triangles: 161 and 225","Kobon records broken: 23 lines make 161, 27 lines make 225","Automated search finds optimal Kobon arrangements for 23 and 27 lines","New Kobon results: SAT solver hits upper bounds for 23 and 27 lines","Kobon triangle puzzle solved for 23 and 27 lines via SAT"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the heuristic straightening step really produces straight lines satisfying the table's ordering constraints for 23 and 27 lines; the paper gives no exact coordinates or certificates, only near-zero values of a numerically minimized target function, and if that fitting fails the claimed proofs of N(23) = 161 and N(27) = 225 collapse.","fun_headline_variants_meta":{"raw":{"variants":["SAT and heuristics yield optimal Kobon triangles: 161 and 225","Kobon records broken: 23 lines make 161, 27 lines make 225","Automated search finds optimal Kobon arrangements for 23 and 27 lines","New Kobon results: SAT solver hits upper bounds for 23 and 27 lines","Kobon triangle puzzle solved for 23 and 27 lines via SAT"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000809,"raw_usage":{"total_tokens":3522,"prompt_tokens":890,"completion_tokens":2632,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":506,"completion_tokens_details":{"reasoning_tokens":2539}},"tokens_in":506,"tokens_out":2632,"duration_ms":17831,"temperature":1.0,"reasoning_tokens":2539,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T18:28:05.152964+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run an independent exact-arithmetic check on the Appendix C tables for 23 and 27 lines: attempt to solve for line angles and offsets so that every prescribed crossing order and triangle-side condition holds with zero violation, or produce a realizability certificate for those tables. If no such exact configuration exists, or if a consistency contradiction is found between the table and the geometry of straight lines, the central claims N(23) = 161 and N(27) = 225 are false.","supporting_citations":[{"cited_title":"Cl´ ement and J","cited_arxiv_id":null,"evidence_quote":"Supplies the upper bound N(n) ≤ n(n−2)/3 for the residue classes that the new 23- and 27-line tables attain."},{"cited_title":"On simple arrangements of lines and pseudo-lines in P2 and R2 with the maximum number of triangles","cited_arxiv_id":null,"evidence_quote":"Gives the combinatorial setting of simple arrangements with the maximum number of triangles and the normal form used for the special arrangements."},{"cited_title":"arminbiere/kissat","cited_arxiv_id":null,"evidence_quote":"The SAT solver that finds satisfying assignments for the generated CNF table problems."},{"cited_title":"Sat-based solver for the kobon triangle problem using kissat and lineorder","cited_arxiv_id":null,"evidence_quote":"The accompanying CNF generator that encodes optimal Kobon arrangements and produces candidate tables."},{"cited_title":"Lineorder - a tool for finding straight line arrangements from pseudolines and generating svg visuals","cited_arxiv_id":null,"evidence_quote":"The accompanying straightening tool that recovers straight-line arrangements from table candidates, including the new 23- and 27-line results."},{"cited_title":"Kobon triangles","cited_arxiv_id":null,"evidence_quote":"Provides the 16-line example used to construct the even 24-line arrangement by inserting an additional line."}],"review_version":1}