{"id":"55eec564-1168-4c5b-8fb0-1240393e58a0","arxiv_id":"2507.17780","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"partial","parameter_count":0,"one_line_summary":"Four machine-generated open conjectures relating independence, zero forcing, domination, and matching invariants in graphs are presented, each with empirical support but no proof.","lead":"This paper presents four new open conjectures in graph theory, all generated by the automated conjecturing system TxGraffiti. These machine-found inequalities connect basic graph invariants and may interest mathematicians and AI researchers studying computer-aided discovery.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Conjecture 1 is false as stated for K2, so the paper's central claim that all four conjectures are open cannot stand.","rationale":"The reader's concern about same-dataset validation is legitimate but secondary. A single explicit counterexample is decisive: the paper's headline contribution is four open conjectures, and one of them is false as written. The Lean statement for conjecture_one also asserts the false proposition if its definitions match the paper's, so formalization via 'sorry' does not rescue the claim. I therefore recommend REJECT for the manuscript as written, rather than CONDITIONAL, because supplying a dataset or an independent test set would not fix the false inequality. If the authors intended a modified claim excluding order-2 graphs or requiring Delta >= 2, that is a new statement requiring new empirical support and a revised exposition.","tokens_in":7711,"tokens_out":7654,"duration_ms":85721,"concrete_test":"Compute alpha, a, R, and Delta for K2 exactly from the definitions in Section 2.1: m=1, degrees [1,1], so a=1; Havel-Hakimi residue R=1; Delta=1; alpha=1. Evaluate Conjecture 1: 1 >= (1+1)/1 = 2 is false. To settle the central claim, the authors must either identify an explicit hidden assumption excluding K2 or provide a corrected statement and rerun an independent enumeration, e.g., all connected graphs up to order 10, to show that the corrected version survives.","verdict_should_be":"REJECT","load_bearing_attack":"Conjecture 1 in Section 2.1 is not open: it fails on K2 under the definitions given in the same section. For K2, n=2, m=1, degrees (1,1), so a(K2) = max{j : sum of the j smallest degrees <= 1} = 1. The Havel-Hakimi process gives R(K2)=1: starting from [1,1], remove the largest entry 1 and subtract 1 from the next 1 entry, leaving [0], which has one zero. Delta(K2)=1 and alpha(K2)=1, so (a+R)/Delta = (1+1)/1 = 2, and the asserted inequality alpha(G) >= (a(G)+R(G))/Delta(G) reads 1 >= 2, which is false. K2 is a nontrivial connected graph under the standard terminology the paper uses, and the paper gives no exclusion of order-2 graphs. Thus at least one of the four 'open' conjectures has a two-vertex counterexample, contradicting the abstract's claim that these statements 'defy both proof and counterexample.' This is not a dataset-circularity concern; it is a direct falsification of the stated conjecture. If the authors intended to require order at least 3 or Delta >= 2, that hypothesis is absent from Conjecture 1 and would need to be stated and re-validated.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript presents four graph-theoretic inequalities generated by the TxGraffiti automated conjecturing system between 2016 and 2023, describes them as open conjectures, gives partial validation for Conjecture 1, displays an empirical plot for Conjecture 4, and provides Lean 4 statements in an appendix. The paper also situates these conjectures in the longer history of TxGraffiti and lists previously published theorems that originated from the system. The central claims are that each conjecture is concise, grounded in natural graph invariants, empirically validated across hundreds of graphs, and resistant to both proof and counterexample despite extensive effort.","tokens_in":7988,"tokens_out":13266,"duration_ms":133488,"significance":"The project has a credible track record: Table 1 lists nine published or in-press theorems that originated from TxGraffiti, which gives the conjectures a genuine pedigree. If the four statements were correct and open, they would be attractive test cases for automated and human proving, and the Lean-translation appendix would add value. However, the mathematical core is currently compromised by a concrete counterexample to Conjecture 1, and the empirical support is largely circular and underdocumented. The paper needs correction and additional evidence before the central claims can be accepted.","major_comments":[{"comment":"As stated, Conjecture 1 is false. For G = K2, we have n = 2, m = 1, degree sequence [1,1], so a(G) = 1 (since 1 <= 1 but 2 > 1), R(G) = 1 (the Havel-Hakimi process sends [1,1] to [0]), Delta(G) = 1, and alpha(G) = 1. The claimed inequality reads 1 >= (1+1)/1 = 2, which is false. K2 is a nontrivial connected graph under the standard convention, and the statement contains no exclusions. The subsequent partial result in the same section explicitly assumes Delta(G) >= 2 in the regular bipartite case, suggesting the exceptional case was recognized. Please add the missing hypothesis (e.g., Delta(G) >= 2 or |V(G)| >= 3), update the abstract, Conjecture 1, and the Lean statement in Appendix A, and re-run the empirical validation under the corrected hypothesis.","section":"Section 2.1, Conjecture 1"},{"comment":"The empirical validation is selection-circular and not fully documented. The conjectures were generated by TxGraffiti from precomputed datasets, and Figure 1 validates Conjecture 4 on the same 335 graphs from the TxGraffiti dataset; a search that selects inequalities on the basis of holding on a dataset cannot be independently confirmed on that same dataset. The paper provides no dataset, no search bounds, and no validation counts for Conjectures 1-3. Please provide the dataset or a reproducible generator, report validation statistics for all four conjectures, and include an out-of-sample check (for example, exhaustive enumeration of all connected graphs up to order 10, or random graphs held out from the generation process).","section":"Section 2.4, Figure 1"},{"comment":"The Lean statements do not match the conjectures stated in the text. In conjecture_two, hypotheses h2 and h3 require max_degree G = min_degree G and max_degree G = 3, which restricts the statement to cubic graphs, whereas Conjecture 2 is for all connected graphs with Delta(G) <= 3. In conjecture_one, h2 : order G >= 1 is weaker than the intended nontrivial condition (order at least 2) and omits the Delta(G) >= 2 hypothesis needed to avoid the K2 counterexample. As written, the appendix does not support the claim that the conjectures have been accurately translated into Lean 4.","section":"Appendix A, Listing 1"}],"minor_comments":[{"comment":"The term 'nontrivial connected graph' is ambiguous; define it explicitly (e.g., |V(G)| >= 2, or after the revision, |V(G)| >= 3 with Delta(G) >= 2) so that the K2 case is treated unambiguously.","section":"Section 2.1"},{"comment":"The term 'König-Egerváry graph' is used without definition or reference; add a one-sentence definition or citation.","section":"Section 2.1"},{"comment":"The phrase 'If G is an r-regular graph G with r > 0' contains a duplicated 'G'; rephrase to 'If G is an r-regular graph with r > 0'.","section":"Section 2.3"},{"comment":"The axes appear to show only numeric scales without clear titles; add explicit axis titles for H(G) and mu*(G) to make the plot self-contained.","section":"Figure 1"},{"comment":"The title contains a stray space in 'Ten Y ears'; correct it to 'Ten Years'.","section":"Title page"}],"recommendation":"major_revision","confidential_remarks":"The K2 counterexample is particularly damaging because the authors explicitly discuss a Delta(G) >= 2 caveat in their partial proof for regular bipartite graphs, so the omission from the conjecture statement appears to be an oversight rather than a deep flaw. The paper is short and more of an experimental-data paper than a traditional theorem paper; if the authors supply reproducible validation and correct the formalizations, it could be suitable as a cs.DM contribution. I do not see grounds for rejecting the entire project, but the current version cannot be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper's central selling point — four machine-generated conjectures that have defied proof and counterexample for years — collapses on the first one. Conjecture 1, as stated for every nontrivial connected graph, is false on K2. For K2, n=2, m=1, degrees (1,1), so a=1, R=1, Δ=1, and α=1. The asserted inequality α ≥ (a+R)/Δ reads 1 ≥ 2. That's a clean, two-vertex counterexample, and the paper gives no exclusion for order 2 or Δ=1. The Lean formalization in Appendix A actually makes the hypothesis weaker (order ≥ 1), so the formal statement is false too. The abstract's claim that these statements 'defy both proof and counterexample' is wrong for at least one of them.\n\nWhat the paper does well: the other three conjectures are plausible and look new. Conjecture 4, linking µ* to the harmonic index, is a genuinely unusual pairing. The partial results in Section 2.1 (regular bipartite, cubic König-Egerváry) are real mathematics, and Table 1 gives a fair record of TxGraffiti's earlier successes. That table is probably the most useful part for readers outside the group.\n\nSoft spots, in proportion. The dataset circularity the reader flagged is real but secondary: the same dataset that generated the conjectures is used for validation, and no data or search bounds are given. That would matter even if Conjecture 1 were true. But the K2 counterexample is not circularity; it is a direct falsification and it dooms the paper in its current form. The fix is easy — add Δ(G) ≥ 2 or order ≥ 3 to Conjecture 1 — but then the abstract and the 'open since 2016' framing need to be adjusted, and the conjecture should be re-validated under the corrected hypothesis.\n\nWho gets value from this paper? People working on automated conjecture generation and on these graph invariants would like the three surviving conjectures and the table. But as submitted, the paper is not reliable. A serious referee would reject it, and a desk editor should not send a paper with a two-vertex counterexample to its main conjecture into review, even if the broader topic is worth attention.\n\nRecommendation: reject for now, but invite a resubmission once Conjecture 1 is corrected, the data is provided, and the validation methodology is documented. The paper might be worth reading then.","headline":"The paper's flagship claim is false: Conjecture 1 fails on K2, so the four open conjectures are not all open as stated.","tokens_in":8481,"tokens_out":2642,"would_cite":false,"duration_ms":28574,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":false},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["05C69","05C70","05C07"],"pacs":[],"model":"deepseek-v4-flash","headline":"The authors present four open graph-theoretic conjectures generated by TxGraffiti over a decade—simple, sharp, and empirically validated—and they argue these are genuine products of human-machine collaboration.","keywords":["automated conjecturing","TxGraffiti","graph theory","independence number","zero forcing","maximal matching","harmonic index","open problems"],"falsifier":"Enumerate all connected simple graphs up to order 10 (or 11) and compute, for each, the invariants $\\alpha$, $a$, $R$, $Z$, $i$, $\\mu^*$, and $H$; a single graph violating any of the four inequalities would refute that conjecture, and for Conjecture 2 the restricted family $\\Delta(G) \\le 3$, $G \\not\\simeq K_4$ could be decided exactly by this census.","tokens_in":7515,"feed_emoji":"🤖","tokens_out":13514,"duration_ms":122281,"temperature":0.7,"pith_summary":"These authors report four open conjectures in graph theory that were generated by TxGraffiti, an automated conjecturing program, and have resisted proof and counterexample for years. Each conjecture is a short inequality pairing natural graph invariants: independence number against a combination of annihilation number and residue; zero forcing number against independence number; independent domination number against minimum maximal matching; and minimum maximal matching against harmonic index. The paper's evidence is empirical—all four hold on the hundreds of graphs in the system's dataset, with equality on structured families—and the authors argue that their simplicity, sharpness, and durability make them worthwhile targets for human and machine mathematicians. If the conjectures are true, they would show that a machine's pattern search can produce statements that sit at the edge of current knowledge.","feed_headline":"A machine's four graph conjectures have stayed open for a decade","feed_subtitle":"Four simple inequalities linking independence, zero forcing, matchings, and the harmonic index remain open.","key_machinery":"The carrier of the argument is TxGraffiti's generate-and-filter loop: from precomputed tables of graph invariants, the system combines expressions symbolically and keeps only empirically valid inequalities, ranking them by sharpness—how often equality is attained in its dataset of hundreds of graphs. The four conjectures are the surviving objects, and each pairs invariants of distinct flavors: the independence number $\\alpha$ with the degree-sequence invariants $a$ and $R$; the zero forcing number $Z$ with $\\alpha$; the independent domination number $i$ with the minimum maximal matching number $\\mu^*$; and $\\mu^*$ with the harmonic index $H$. The paper also uses the identity $\\mu^*(G)=i(L(G))$ to connect the matching-based parameters to domination in line graphs, and it treats equality examples as structural hints for future proofs.","core_discovery":"At the center of the paper is the claim that four inequalities, each produced by TxGraffiti between 2016 and 2023, are genuine open problems. For a nontrivial connected graph $G$, the conjectures state: $\\alpha(G) \\ge (a(G)+R(G))/\\Delta(G)$, and for connected graphs with $\\Delta(G) \\le 3$ other than $K_4$, $Z(G) \\le \\alpha(G)+1$; for $r$-regular graphs with $r>0$, $i(G) \\le \\mu^*(G)$; and for every nontrivial connected graph, $\\mu^*(G) \\le H(G)$. The authors give partial evidence: regular bipartite graphs and certain cubic graphs satisfy the first, claw-free cubic graphs satisfy the second, 2-regular graphs satisfy the third, and the fourth holds with equality on structured families in the dataset. They stress that every statement is simple, sharp, empirically valid on hundreds of graphs, and still open despite sustained attention.","pith_inferences":["If the four conjectures all hold, it would suggest that simple arithmetic combinations of classical invariants are an abundant source of open problems, and that the bottleneck will shift from generating conjectures to resolving them.","A natural stress test is to run the same inequality search on graph families the current dataset undersamples—highly irregular graphs for Conjecture 1, subcubic graphs with many degree-2 vertices for Conjecture 2, and high-degree regular graphs for Conjecture 3.","The authors' narrative implies a new criterion for evaluating conjecturing software: not only theorems proved, but the durability and perceived naturalness of the open problems it leaves behind. A longer-term test is whether these four conjectures, or descendants of them, eventually fall to human or machine proof."],"forward_implications":["If Conjecture 1 is true, then every nontrivial connected graph has a lower bound on $\\alpha(G)$ computable directly from its degree sequence, strengthening the classical $\\alpha \\ge R$ inequality.","If Conjecture 2 is true, then for connected subcubic graphs, the zero forcing number is determined within one of the independence number (except at $K_4$), giving a tight bridge between a linear-algebraic parameter and a packing parameter.","If Conjecture 3 is true, then in every regular graph the smallest maximal independent set is no larger than the smallest maximal matching, extending the known $\\alpha(G) \\le \\mu(G)$ phenomenon from maximum packings to saturated packings.","If Conjecture 4 is true, then the discrete minimum maximal matching number is bounded by the continuous harmonic index for every connected graph, opening a quantitative link between chemical graph indices and domination-theoretic parameters.","Because all four are formalized in a proof assistant, any one of them being proved or refuted would give a concrete data point on whether machine-generated conjectures accelerate mathematical research."],"supporting_citations":[{"why":"Introduces the residue invariant used in Conjecture 1 and the automated conjecturing paradigm.","marker":"Fajtlowicz [1988]"},{"why":"Introduces the annihilation number used in Conjecture 1.","marker":"Pepper [2004]"},{"why":"Proves the known inequality $\\alpha(G) \\ge R(G)$ that Conjecture 1 extends.","marker":"Favaron et al. [1991]"},{"why":"States the constructive degree-sequence reduction used to define the residue.","marker":"Havel [1955]"},{"why":"Supplies the degree-sequence realizability criterion behind the residue computation.","marker":"Hakimi [1962]"},{"why":"Introduces the zero forcing number $Z(G)$ central to Conjecture 2.","marker":"Barioli et al. [2008]"},{"why":"Proves a claw-free cubic special case of Conjecture 2.","marker":"Davila and Henning [2020]"},{"why":"Proves $\\alpha(G) \\le \\mu(G)$ for regular graphs, the analogue that frames Conjecture 3.","marker":"Caro et al. [2022b]"},{"why":"Conjectures earlier bounds on $\\mu^*(G)$, the saturation parameter in Conjectures 3 and 4.","marker":"DeLaViña et al. [2007]"}],"fun_headline_variants":["Machine's four graph conjectures remain open for a decade","Four open conjectures from TxGraffiti, unresolved since 2016-2023","Decade-old machine conjectures: still open, still sharp","Machine collaborator's four graph inequalities stay open","TxGraffiti's four open problems in graph theory, ten years on"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The case rests on the assumption that the hundreds of graphs in TxGraffiti's dataset are a representative test bed, so the absence of counterexamples there is meaningful evidence for the four inequalities, and that the authors' claim that the statements remain open is accurate.","fun_headline_variants_meta":{"raw":{"variants":["Machine's four graph conjectures remain open for a decade","Four open conjectures from TxGraffiti, unresolved since 2016-2023","Decade-old machine conjectures: still open, still sharp","Machine collaborator's four graph inequalities stay open","TxGraffiti's four open problems in graph theory, ten years on"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000439,"raw_usage":{"total_tokens":2209,"prompt_tokens":903,"completion_tokens":1306,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":519,"completion_tokens_details":{"reasoning_tokens":1217}},"tokens_in":519,"tokens_out":1306,"duration_ms":10986,"temperature":1.0,"reasoning_tokens":1217,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T14:56:02.410240+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate all connected simple graphs up to order 10 (or 11) and compute, for each, the invariants $\\alpha$, $a$, $R$, $Z$, $i$, $\\mu^*$, and $H$; a single graph violating any of the four inequalities would refute that conjecture, and for Conjecture 2 the restricted family $\\Delta(G) \\le 3$, $G \\not\\simeq K_4$ could be decided exactly by this census.","supporting_citations":[],"review_version":1}