{"id":"495ea750-2194-4b12-8577-61abee4ecf5b","arxiv_id":"2608.10028","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper gives a human-checkable proof that the recently announced 112-vertex graph is a genuine counterexample to Jaeger's Petersen coloring conjecture.","lead":"A new hand-checkable proof confirms that a specific 112-vertex graph cannot be colored in the way Jaeger's Petersen coloring conjecture predicted. It matters because it offers an independent, non-SAT verification and identifies reusable gadgets for studying similar graph coloring questions.","discovery_kind":"replication","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The proof hinges on Lemma 2.1's Table 1: the 55 negative rows are asserted without derivation, and any hidden valid P-coloring of F would break the R-relations used in Lemma 2.2 and Theorem 2.3.","rationale":"The reader's weakest assumption points to Table 1's completeness as the main residual doubt, and my independent reading locates the same bottleneck. I examined the subsequent logical structure: the derivation of relations (2) and (3) from Lemma 2.1 is valid, the eight cases in Lemma 2.2 use the R-relations consistently, and each row of Table 2 checks out. The final step, a K4 in Q from four pairwise adjacent colors, is sound because Petersen is triangle-free and cubic. No other internal inconsistency surfaced, and the proof does not depend on circular reasoning: it is a self-contained construction, albeit one whose foundation is a finite table. Since the paper is explicitly presented as human-checkable, the absence of justifications for the 55 negative rows is a genuine, if narrow, gap. A small independent enumeration would remove it; unless that check is run, the conditional verdict is appropriate. The reader's secondary concern about the symmetry reduction is not warranted, but the primary concern remains shared, so no verdict change is needed.","tokens_in":10309,"tokens_out":32793,"duration_ms":262288,"concrete_test":"Run an independent exhaustive backtracking search over all P-colorings of F that respect the fixed values in each of the 64 rows of Table 1. For each row, enumerate the remaining unknowns σ(56), σ(58), σ(i2), σ(36), σ(i1) under the star constraints at vertices 3,5,6,8, and check that the row has a completion if and only if it is one of the 9 listed rows, with exactly the listed completion. Also verify the stated 'at most one' claim. This directly settles whether Lemma 2.1 holds; if the enumeration matches Table 1, the R-relations and the rest of the proof are sound.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 2.1 is the load-bearing step. Its proof reduces to Table 1: after fixing σ(12)=e1, σ(24)=e2, σ(27)=e3, the six edge colors at vertices 1,4,7 give 64 rows; the paper asserts that exactly 9 extend to a P-coloring of F and that each extension is unique. The 55 dash rows carry no individual derivation, so the lemma's trichotomy (dist 0, 1, 2 and the two options at dist 2) is supported only by the completeness of this table. Lemma 2.2 then converts Lemma 2.1 into the R-relations (1)-(3); every case in Lemma 2.2 and every row of Table 2 calls on those relations. I checked the Table 2 case analysis and the derivation of (2),(3) from Lemma 2.1; they appear internally consistent. The bottleneck is therefore purely the unverified 64-case enumeration. A single dash that actually admits a completion would change the set R for that input pair, could eliminate or add cases in Lemma 2.2, and could make the final K4 contradiction unsound. This is a correctness risk, not a disagreement with the P-coloring conjecture; if the table is right, the proof establishes the counterexample. The secondary symmetry reduction in Lemma 2.1 is valid, since Petersen's automorphism group is transitive on ordered stars, so I do not share that doubt.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper provides a hand-checkable proof that the 112-vertex cubic bridgeless graph recently proposed by Putman is a counterexample to Jaeger's Petersen coloring conjecture. The proof first analyzes P-colorings of a 4-pole F obtained by deleting two adjacent vertices from the Petersen graph, encoding the outcome in a 64-row table (Lemma 2.1). It then derives transfer relations for a 36-vertex 4-pole L built from four copies of F (Lemma 2.2). Three copies of L are joined to a claw to form the 112-vertex graph G; assuming a P-coloring of G, the paper derives that four edges of the Petersen graph must be pairwise adjacent in its line graph Q, contradicting the fact that Q has no K4. The final contradiction is short and structural, and the proof does not rely on a SAT solver.","tokens_in":10604,"tokens_out":11155,"duration_ms":109917,"significance":"If the proof is correct, this paper gives the first counterexample to a longstanding conjecture and, more importantly, explains the counterexample through reusable multipole behavior rather than a large SAT computation. The final argument using the clique number of the line graph of the Petersen graph is elegant, and the reduction to small finite cases is a genuine methodological contribution. The proof has no fitted parameters and does not assume non-colorability of the target graph. The main caveat is that the load-bearing finite enumeration in Lemma 2.1 is not fully exhibited; the contribution is therefore conditional on completing that verification.","major_comments":[{"comment":"The entire proof hinges on the assertion that, after fixing σ(12)=e1, σ(24)=e2, and σ(27)=e3, exactly 9 of the 64 enumerated assignments around vertex 2 extend to a P-coloring of F, and that in each of these 9 cases the extension is unique. Table 1 displays the 9 completed rows, but the 55 rows marked with dashes contain no derivation or certificate showing that no completion exists. Since equations (1)–(3), Lemma 2.2, Table 2, and Theorem 2.3 all depend on Lemma 2.1, a single hidden valid completion among those 55 rows would invalidate the main result. Please provide an explicit checkable argument for each dash row, or include a machine-verifiable certificate together with a clear explanation of how it establishes the negative cases; in its current form the table is an assertion rather than a human-checkable proof.","section":"§2, Lemma 2.1 and Table 1"},{"comment":"Lemma 2.2 states implications conditional on dist(σ(i1(L)),σ(i2(L))) being 0, 1, or in {2,3}, but it does not explicitly state that these are the only possible values for a P-coloring of L. Theorem 2.3 relies on this exhaustiveness when it enumerates only δ1,δ2 ∈ {0,1,{2,3}} in Table 2. The proof of Lemma 2.2 appears to establish exhaustiveness through the S/O case analysis, but the lemma should state it explicitly (for example, 'for every P-coloring of L, the distance is 0, 1, 2, or 3'), and the proof should flag where this is concluded. Without such a statement, the step 'the nine cases' in Theorem 2.3 is not formally justified.","section":"§2, Lemma 2.2 and Theorem 2.3"}],"minor_comments":[{"comment":"The reduction 'by symmetry of P, without loss of generality σ(12)=e1, σ(24)=e2, σ(27)=e3' should be justified with a sentence on the ordered-star transitivity of Aut(P), so that the reader can verify that Table 1 indeed covers all possible colorings of the star at vertex 2.","section":"§2, Lemma 2.1"},{"comment":"In the sentence 'Since δ1=0, Lemma 2.2 gives σ(i1_1)=σ(i1_2)...', the equality σ(i1_1)=σ(i1_2) follows directly from the definition of δ1; Lemma 2.2 provides the distance statement dist(σ(i1_1),σ(o1_1))=1. Please rephrase to avoid attributing the equality to Lemma 2.2.","section":"§2, Theorem 2.3"},{"comment":"There are typographical spacing issues in 'on112vertices' and 'the4-poleF'; please insert spaces before the numbers.","section":"Abstract and Introduction"},{"comment":"The paragraph introducing the cases S and O is terse. The phrase 'the other endpoint in P of the label on the edge to c is used' would be clearer if S and O were defined formally as conditions on the ordered pair of labels at each leaf of the claw.","section":"§2, Lemma 2.2"}],"recommendation":"major_revision","confidential_remarks":"This is a potentially important paper. My main concern is the unexhibited 55-row negative verification in Table 1; if the author can supply that verification, the result is likely publishable. I do not think the paper should be rejected outright, because the gap is local and fixable within the manuscript's scope. The AI-assisted-writing disclosure is transparent and does not affect my assessment."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The one thing you should know: this paper does not contain a new counterexample. It contains a new proof of Putman's 112-vertex counterexample, and the proof is mostly checkable by hand. That is still valuable, because the original proof relied on a 68,324-clause SAT run. This paper replaces that with a few multipole lemmas and a clean final contradiction.\n\nWhat it does well: Lemma 2.1 characterizes all P-colorings of the 4-pole F, Lemma 2.2 turns that into a compact relation for the 36-vertex gadget L, and Theorem 2.3 assembles three copies of L into a graph where the P-coloring constraints force a K4 in the line graph of the Petersen graph. The final contradiction is elegant and sound. I went through the eight-case analysis in Lemma 2.2 and the nine-case table in Theorem 2.3; they are internally consistent and all follow from Lemma 2.1. The paper also gives proper credit to Putman and does not oversell novelty. The symmetry reduction in Lemma 2.1 is valid: the Petersen graph's automorphism group is transitive on ordered stars, so 'by symmetry of P' is not a real gap.\n\nThe soft spot is exactly one table. Lemma 2.1 is the load-bearing step, and its proof rests on Table 1: after fixing three edge colors at vertex 2, the paper lists 64 assignments of the remaining edge colors at vertices 1, 4, and 7. Nine rows are explicitly completed; the other 55 are dashes with a sentence saying they cannot be completed. No derivation is given for any of those 55 negative rows. The rest of the paper does not care which specific assignment fails—it only needs the trichotomy that Lemma 2.1 asserts. But if even one dash actually admitted a completion, the relation R in Lemma 2.2 would change, and the final K4 contradiction could break. This is a real correctness risk, not a stylistic quibble. The paper would be substantially stronger with an appendix containing, for each of the 55 rows, a short reason (or a machine-checkable certificate) for why it fails.\n\nWho should read this: graph theorists working on snarks, normal edge-colorings, and the Petersen coloring conjecture. It is also a nice case study in replacing SAT certificates with human-readable arguments. It deserves peer review. The referee should ask for the missing verification of Table 1's negative rows, but the main argument is solid enough that I would not desk-reject it.","headline":"A genuinely human-checkable proof of Putman's 112-vertex Petersen-coloring counterexample, with one load-bearing finite table that should be independently verified before publication.","tokens_in":11140,"tokens_out":1856,"would_cite":true,"duration_ms":20960,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["05C15"],"pacs":[],"model":"deepseek-v4-flash","headline":"A short, hand-checkable proof confirms the 112-vertex counterexample to the Petersen coloring conjecture.","keywords":["Petersen coloring conjecture","snark","normal edge-coloring","bridgeless cubic graph","line graph of the Petersen graph","gadget proof","112-vertex counterexample"],"falsifier":"Exhibit a Petersen coloring of G — a consistent assignment of each edge of G to an edge of the Petersen graph and each vertex to a vertex such that incident triples map to incident triples; a single such assignment disproves Theorem 2.3.","tokens_in":10066,"feed_emoji":"🎨","tokens_out":9939,"duration_ms":97496,"temperature":0.7,"pith_summary":"The paper proves a specific claim: the 112-vertex cubic bridgeless graph recently exhibited in a preprint has no Petersen coloring. If the proof is correct, the Petersen coloring conjecture — that every bridgeless cubic graph admits such a coloring — is false. The argument replaces a 68,324-clause SAT unsatisfiability check with a small, hand-checkable case analysis of how the construction's multipole gadgets can be colored, then derives the final contradiction from the fact that the line graph of the Petersen graph contains no clique on four vertices. This matters because the conjecture, if true, would have implied the Berge-Fulkerson conjecture and the 5-cycle double cover conjecture; a counterexample removes that route and focuses attention on which subclasses of cubic graphs are Petersen-colorable.","feed_headline":"112-vertex graph refutes Petersen coloring conjecture","feed_subtitle":"A short finite case check replaces the original 68,324-clause SAT proof, confirming the counterexample by hand.","key_machinery":"The central object is the 4-pole F, obtained by deleting two adjacent vertices from the Petersen graph P and leaving four semi-edges; Lemma 2.1 classifies how a P-coloring of F can assign edge labels to those semi-edges, with the relation R(g,h) encoding allowed output pairs depending on whether the input labels are at distance 0, 1, 2, or 3 in the line graph Q = L(P). The 4-pole L, made from four copies of F joined to a claw, then has the forced behavior described in Lemma 2.2: its output semi-edges are determined by its input semi-edges up to a small list. The final contradiction is structural: the constraints from three L-copies force four edges of P to be pairwise adjacent, but Q has no 4-clique.","core_discovery":"The central discovery is Theorem 2.3: there exists a cubic bridgeless graph G on 112 vertices that admits no P-coloring, meaning no total map taking edges of G to edges of the Petersen graph P and vertices of G to vertices of P so that each vertex's incident edges map to the three edges incident with a single vertex of P. The proof establishes this by first classifying the P-coloring behavior of the 4-pole F (P with two adjacent vertices removed) through a 64-case enumeration, then showing that a 36-vertex 4-pole L built from four copies of F has the forcing behavior described in Lemma 2.2. Three copies of L are wired together with a claw to form G; applying Lemma 2.2 forces four edges of P to be pairwise adjacent in the line graph Q = L(P), which is impossible because Q has no 4-clique. The proof is fully finite and does not rely on a SAT solver.","pith_inferences":["The same gadget structure might yield smaller counterexamples: since the proof only uses the forced adjacency pattern at the end, one could search over graphs assembled from L-copies to minimize vertex count.","The proof suggests a sufficient condition for non-P-colorability: a bridgeless cubic graph whose P-coloring constraints force four edges of the Petersen graph to be pairwise adjacent contradicts the clique number of the line graph, so any such constructed graph is a counterexample.","The table-driven method could be partially mechanized at a much smaller scale: checking the 64 cases of Lemma 2.1 is a task a reader can do by hand, and the same template could generate proofs for larger gadgets.","If future work finds a smaller counterexample, this proof provides the template: isolate a small multipole whose colorings are finitely classifiable, combine them, and reduce the contradiction to a known structural property of the target graph."],"forward_implications":["The Petersen coloring conjecture is false: not every bridgeless cubic graph admits a Petersen coloring.","The 112-vertex graph's status as a counterexample no longer rests on a SAT computation; its non-colorability is established by a finite case analysis.","The implication chain from the Petersen coloring conjecture to the Berge-Fulkerson conjecture and the 5-cycle double cover conjecture is no longer available; those conjectures remain open and need independent approaches.","The 4-pole gadgets F and L, with their classified coloring behaviors, are reusable building blocks for constructing and testing other cubic graphs for Petersen colorability.","Any graph assembled to force four edge labels to be pairwise adjacent in the line graph of the Petersen graph will be non-P-colorable in the same way."],"supporting_citations":[{"why":"Supplies the 112-vertex graph and the SAT-unsatisfiability result that the paper reproves by hand.","marker":"[13]"},{"why":"States the Petersen coloring conjecture whose falsehood the counterexample establishes.","marker":"[5]"},{"why":"Describes the machine-checkable certificate format used for SAT verification, the computation-heavy alternative this proof replaces.","marker":"[15]"}],"fun_headline_variants":["Hand-checkable proof confirms 112-vertex counterexample","Petersen conjecture refuted by finite case check, no SAT","112-vertex graph: counterexample proven without SAT solver","Human proof replaces 68k-clause SAT for Petersen counterexample"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The entire proof leans on the correctness and completeness of the 64-row table in the appendix: if any of the 55 rows marked with a dash actually extends to a Petersen coloring of the 4-pole F, then the gadget lemmas and the final contradiction no longer follow.","fun_headline_variants_meta":{"raw":{"variants":["Hand-checkable proof confirms 112-vertex counterexample","Petersen conjecture refuted by finite case check, no SAT","112-vertex graph: counterexample proven without SAT solver","Human proof replaces 68k-clause SAT for Petersen counterexample"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000454,"raw_usage":{"total_tokens":2242,"prompt_tokens":868,"completion_tokens":1374,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":484,"completion_tokens_details":{"reasoning_tokens":1303}},"tokens_in":484,"tokens_out":1374,"duration_ms":11969,"temperature":1.0,"reasoning_tokens":1303,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T04:21:47.681270+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a Petersen coloring of G — a consistent assignment of each edge of G to an edge of the Petersen graph and each vertex to a vertex such that incident triples map to incident triples; a single such assignment disproves Theorem 2.3.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the 112-vertex graph and the SAT-unsatisfiability result that the paper reproves by hand."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"States the Petersen coloring conjecture whose falsehood the counterexample establishes."},{"cited_title":"Wetzler, M.J.H","cited_arxiv_id":null,"evidence_quote":"Describes the machine-checkable certificate format used for SAT verification, the computation-heavy alternative this proof replaces."}],"review_version":1}