Petersen coloring conjecture

Overview

Known

A source-reported 112-vertex counterexample refutes the universal coloring conjecture. A second nonisomorphic witness is separately certified; neither establishes the smallest possible order.

Every bridgeless cubic graph admits a Petersen coloringDisprovedPutman 2026
The main 112-vertex counterexampleProvedPutman 2026
A distinct symmetric 112-vertex counterexampleProvedPutman 2026

Latest

Two explicit counterexamples and certificatesAug 8, 2026

An edge-star mapping question, answered negatively by a finite source-reported obstruction.

Precise statement · Exact conventions and hypotheses

A Petersen coloring maps edges of a finite loopless cubic graph G to edges of the Petersen graph P. At each vertex of G, its three incident edges must map bijectively onto the three edges incident with some vertex of P. This is a local edge-star condition, not a proper three-edge-coloring. The reported witness is simple and connected; it therefore refutes the broader bridgeless cubic assertion.

A 112-Vertex Counterexample to the Petersen Coloring Conjecture →

Definitions

Incident edge-star: The three edges meeting a cubic vertex. A Petersen coloring sends this whole set bijectively to the star at a vertex of the Petersen graph.
A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
Bridgeless cubic graph: Every vertex has degree three, and removing any one edge does not disconnect its component. The reported witnesses are simple and connected.
A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
Introduction; Proposition 2.1; references to Jaeger (1985, 1988) →
Theorem 1.1; Section 3; Appendix A →

Question paraphrased by OpenMath. Original wording is available in the sources.

Landscape

Figures and explorable examples. Selecting a statement opens its exact wording.

The 112-vertex counterexample

Every vertex has degree three and no single edge disconnects the graph, yet no map to the Petersen graph preserves its edge-stars.

Main witness G = 3L + C

Positions come from a computed layout and carry no meaning; only the edges do. The picture cannot show that no Petersen coloring exists: that is the cited, formally checked theorem.

This graph has no Petersen coloring and no normal five-edge-coloring.
So not every bridgeless cubic graph is Petersen-colorable.

Dataset petersen-witness-graph v1 · Edges read from the published witness and checked against its SHA-256; layout from the Laplacian's second and third eigenvectors refined by 400 deterministic Fruchterman–Reingold steps. Software: python 3.12.15, numpy 2.3.4. Exact edges; positions rounded to four decimals. SHA-256 bfaaec91ea6b… · Download JSON

Data

Set	Edges
Graph (168 edges)	0–1, 0–5, 0–31, 1–2, 1–6, 2–7, 2–100, 3–5, 3–6, 3–11, 4–6, 4–7, 4–9, 5–7, 8–9, 8–10, 8–11, 9–14, 10–12, 10–20, 11–28, 12–13, 12–17, 13–14, 13–18, 14–19, 15–17, 15–18, 15–22, 16–18, 16–19, 16–56, 17–19, 20–21, 20–25, 21–22, 21–26, 22–27, 23–25, 23–26, 23–30, 24–26, 24–27, 24–39, 25–27, 28–29, 28–33, 29–30, 29–34, 30–35, 31–33, 31–34, 32–34, 32–35, 32–37, 33–35, 36–37, 36–38, 36–39, 37–42, 38–64, 38–92, 39–78, 40–41, 40–45, 40–71, 41–42, 41–46, 42–47, 43–45, 43–46, 43–51, 44–46, 44–47, 44–49, 45–47, 48–49, 48–50, 48–51, 49–54, 50–52, 50–60, 51–68, 52–53, 52–57, 53–54, 53–58, 54–59, 55–57, 55–58, 55–62, 56–58, 56–59, 57–59, 60–61, 60–65, 61–62, 61–66, 62–67, 63–65, 63–66, 63–70, 64–66, 64–67, 65–67, 68–69, 68–73, 69–70, 69–74, 70–75, 71–73, 71–74, 72–74, 72–75, 72–108, 73–75, 76–77, 76–81, 76–107, 77–78, 77–82, 78–83, 79–81, 79–82, 79–87, 80–82, 80–83, 80–85, 81–83, 84–85, 84–86, 84–87, 85–90, 86–88, 86–96, 87–104, 88–89, 88–93, 89–90, 89–94, 90–95, 91–93, 91–94, 91–98, 92–94, 92–95, 93–95, 96–97, 96–101, 97–98, 97–102, 98–103, 99–101, 99–102, 99–106, 100–102, 100–103, 101–103, 104–105, 104–109, 105–106, 105–110, 106–111, 107–109, 107–110, 108–110, 108–111, 109–111

Set

Edges

Graph (168 edges)

0–1, 0–5, 0–31, 1–2, 1–6, 2–7, 2–100, 3–5, 3–6, 3–11, 4–6, 4–7, 4–9, 5–7, 8–9, 8–10, 8–11, 9–14, 10–12, 10–20, 11–28, 12–13, 12–17, 13–14, 13–18, 14–19, 15–17, 15–18, 15–22, 16–18, 16–19, 16–56, 17–19, 20–21, 20–25, 21–22, 21–26, 22–27, 23–25, 23–26, 23–30, 24–26, 24–27, 24–39, 25–27, 28–29, 28–33, 29–30, 29–34, 30–35, 31–33, 31–34, 32–34, 32–35, 32–37, 33–35, 36–37, 36–38, 36–39, 37–42, 38–64, 38–92, 39–78, 40–41, 40–45, 40–71, 41–42, 41–46, 42–47, 43–45, 43–46, 43–51, 44–46, 44–47, 44–49, 45–47, 48–49, 48–50, 48–51, 49–54, 50–52, 50–60, 51–68, 52–53, 52–57, 53–54, 53–58, 54–59, 55–57, 55–58, 55–62, 56–58, 56–59, 57–59, 60–61, 60–65, 61–62, 61–66, 62–67, 63–65, 63–66, 63–70, 64–66, 64–67, 65–67, 68–69, 68–73, 69–70, 69–74, 70–75, 71–73, 71–74, 72–74, 72–75, 72–108, 73–75, 76–77, 76–81, 76–107, 77–78, 77–82, 78–83, 79–81, 79–82, 79–87, 80–82, 80–83, 80–85, 81–83, 84–85, 84–86, 84–87, 85–90, 86–88, 86–96, 87–104, 88–89, 88–93, 89–90, 89–94, 90–95, 91–93, 91–94, 91–98, 92–94, 92–95, 93–95, 96–97, 96–101, 97–98, 97–102, 98–103, 99–101, 99–102, 99–106, 100–102, 100–103, 101–103, 104–105, 104–109, 105–106, 105–110, 106–111, 107–109, 107–110, 108–110, 108–111, 109–111

Check the witness

Recomputed from the published adjacency list: the graph is a simple bridgeless cubic graph with the size, girth and connectivity the statement gives.

Property	Recomputed	Statement
Vertices	112	matches
Edges	168	matches
Every vertex has degree 3	yes	matches
Simple: no loops or parallel edges	yes	matches
Connected	yes	matches
No bridge (removing any one edge)	yes	matches
Edge-connectivity at least 3 (any two edges)	yes	matches
Vertex-connectivity at least 3 (any two vertices)	yes	matches
Girth (shortest cycle)	5	matches

This checks the graph's structure only. That it has no Petersen coloring is the cited theorem and its formal proof; it is not recomputed here.

Visual setup

From the Petersen graph to the obstruction

Construction hierarchy for the main graph: F has 8 vertices, L has 36 and G has 112.

Reading boundary. This diagram shows copy counts, not every semiedge join. Use the exact adjacency list and source construction for the witness.

The main constructionQuestion scope

Construction hierarchy for the main graph: F has 8 vertices, L has 36 and G has 112.

Text version

Deleting two adjacent vertices leaves F. Four F copies and C give L; three L copies and another C give G. The source tables specify the semiedge joins.

Layout is schematic; coordinates and line lengths carry no mathematical scale.

The main construction
Proved
The main 112-vertex counterexample
Scope & assumptions. G is the exact labeled graph in Appendix A; its normalized sorted-edge-list digest identifies the SAT input. No minimum-order claim is made.
The main 112-vertex counterexample →

Sources & review

Authored by OpenMath source curation on 2026-10-14 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

A 112-Vertex Counterexample to the Petersen Coloring ConjectureTheorem 1.1; Section 3; Appendix APreprintOriginal passage ↗
Petersen counterexample: frozen construction and certificates03_CERTIFICATION, 04_OPTIONAL_D3 and 05_DOCUMENTATIONProject documentationOriginal passage ↗

Inspect the main graph

Inspect the exact adjacency

112 numbered vertices and 168 undirected edges.

Vertex

Vertex 0 has neighbors 1, 5, 31.

Complete adjacency table

Every numbered vertex and its neighbors
Vertex	Neighbors
0	1, 5, 31
1	0, 2, 6
2	1, 7, 100
3	5, 6, 11
4	6, 7, 9
5	0, 3, 7
6	1, 3, 4
7	2, 4, 5
8	9, 10, 11
9	4, 8, 14
10	8, 12, 20
11	3, 8, 28
12	10, 13, 17
13	12, 14, 18
14	9, 13, 19
15	17, 18, 22
16	18, 19, 56
17	12, 15, 19
18	13, 15, 16
19	14, 16, 17
20	10, 21, 25
21	20, 22, 26
22	15, 21, 27
23	25, 26, 30
24	26, 27, 39
25	20, 23, 27
26	21, 23, 24
27	22, 24, 25
28	11, 29, 33
29	28, 30, 34
30	23, 29, 35
31	0, 33, 34
32	34, 35, 37
33	28, 31, 35
34	29, 31, 32
35	30, 32, 33
36	37, 38, 39
37	32, 36, 42
38	36, 64, 92
39	24, 36, 78
40	41, 45, 71
41	40, 42, 46
42	37, 41, 47
43	45, 46, 51
44	46, 47, 49
45	40, 43, 47
46	41, 43, 44
47	42, 44, 45
48	49, 50, 51
49	44, 48, 54
50	48, 52, 60
51	43, 48, 68
52	50, 53, 57
53	52, 54, 58
54	49, 53, 59
55	57, 58, 62
56	16, 58, 59
57	52, 55, 59
58	53, 55, 56
59	54, 56, 57
60	50, 61, 65
61	60, 62, 66
62	55, 61, 67
63	65, 66, 70
64	38, 66, 67
65	60, 63, 67
66	61, 63, 64
67	62, 64, 65
68	51, 69, 73
69	68, 70, 74
70	63, 69, 75
71	40, 73, 74
72	74, 75, 108
73	68, 71, 75
74	69, 71, 72
75	70, 72, 73
76	77, 81, 107
77	76, 78, 82
78	39, 77, 83
79	81, 82, 87
80	82, 83, 85
81	76, 79, 83
82	77, 79, 80
83	78, 80, 81
84	85, 86, 87
85	80, 84, 90
86	84, 88, 96
87	79, 84, 104
88	86, 89, 93
89	88, 90, 94
90	85, 89, 95
91	93, 94, 98
92	38, 94, 95
93	88, 91, 95
94	89, 91, 92
95	90, 92, 93
96	86, 97, 101
97	96, 98, 102
98	91, 97, 103
99	101, 102, 106
100	2, 102, 103
101	96, 99, 103
102	97, 99, 100
103	98, 100, 101
104	87, 105, 109
105	104, 106, 110
106	99, 105, 111
107	76, 109, 110
108	72, 110, 111
109	104, 107, 111
110	105, 107, 108
111	106, 108, 109

Construction details and sources ↓

Inspect the symmetric graph

Inspect the exact adjacency

112 numbered vertices and 168 undirected edges.

Vertex

Vertex 0 has neighbors 1, 5, 31.

Complete adjacency table

Every numbered vertex and its neighbors
Vertex	Neighbors
0	1, 5, 31
1	0, 2, 6
2	1, 7, 52
3	5, 6, 11
4	6, 7, 9
5	0, 3, 7
6	1, 3, 4
7	2, 4, 5
8	9, 10, 11
9	4, 8, 14
10	8, 12, 20
11	3, 8, 28
12	10, 13, 17
13	12, 14, 18
14	9, 13, 19
15	17, 18, 22
16	18, 19, 74
17	12, 15, 19
18	13, 15, 16
19	14, 16, 17
20	10, 21, 25
21	20, 22, 26
22	15, 21, 27
23	25, 26, 30
24	26, 27, 109
25	20, 23, 27
26	21, 23, 24
27	22, 24, 25
28	11, 29, 33
29	28, 30, 34
30	23, 29, 35
31	0, 33, 34
32	34, 35, 111
33	28, 31, 35
34	29, 31, 32
35	30, 32, 33
36	37, 41, 67
37	36, 38, 42
38	37, 43, 88
39	41, 42, 47
40	42, 43, 45
41	36, 39, 43
42	37, 39, 40
43	38, 40, 41
44	45, 46, 47
45	40, 44, 50
46	44, 48, 56
47	39, 44, 64
48	46, 49, 53
49	48, 50, 54
50	45, 49, 55
51	53, 54, 58
52	2, 54, 55
53	48, 51, 55
54	49, 51, 52
55	50, 52, 53
56	46, 57, 61
57	56, 58, 62
58	51, 57, 63
59	61, 62, 66
60	62, 63, 110
61	56, 59, 63
62	57, 59, 60
63	58, 60, 61
64	47, 65, 69
65	64, 66, 70
66	59, 65, 71
67	36, 69, 70
68	70, 71, 109
69	64, 67, 71
70	65, 67, 68
71	66, 68, 69
72	73, 77, 103
73	72, 74, 78
74	16, 73, 79
75	77, 78, 83
76	78, 79, 81
77	72, 75, 79
78	73, 75, 76
79	74, 76, 77
80	81, 82, 83
81	76, 80, 86
82	80, 84, 92
83	75, 80, 100
84	82, 85, 89
85	84, 86, 90
86	81, 85, 91
87	89, 90, 94
88	38, 90, 91
89	84, 87, 91
90	85, 87, 88
91	86, 88, 89
92	82, 93, 97
93	92, 94, 98
94	87, 93, 99
95	97, 98, 102
96	98, 99, 111
97	92, 95, 99
98	93, 95, 96
99	94, 96, 97
100	83, 101, 105
101	100, 102, 106
102	95, 101, 107
103	72, 105, 106
104	106, 107, 110
105	100, 103, 107
106	101, 103, 104
107	102, 104, 105
108	109, 110, 111
109	24, 68, 108
110	60, 104, 108
111	32, 96, 108

Construction details and sources ↓

Results

The question 1

Disproved
Every bridgeless cubic graph admits a Petersen coloring
Parallel edges are allowed; the simple connected witness already lies in this class.
Putman 2026
Conjecture · Primary formulation
DisprovedPutman 2026
Every bridgeless cubic graph admits a Petersen coloring
Every finite loopless bridgeless cubic graph admits an edge map to the Petersen graph that maps each incident edge-star bijectively onto a target vertex’s edge-star.
Assumptions
- Parallel edges are allowed; the simple connected witness already lies in this class.
In this problem
Parallel edges are allowed; the simple connected witness already lies in this class.
Sources
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
  - Introduction; Proposition 2.1; references to Jaeger (1985, 1988) →
  - Theorem 1.1; Section 3; Appendix A →
Open statement page →

Equivalent formulations 1

Disproved
Normal five-edge-colorings for bridgeless cubic graphs
A poor edge has three colors across its endpoint stars; a rich edge has five.
Putman 2026
Conjecture · Equivalent formulation
DisprovedPutman 2026
Normal five-edge-colorings for bridgeless cubic graphs
Every finite loopless bridgeless cubic graph has a proper edge-coloring with at most five colors in which the union of the palettes at the endpoints of every edge has either three or five colors.
Assumptions
- A poor edge has three colors across its endpoint stars; a rich edge has five. Four is forbidden.
In this problem
A poor edge has three colors across its endpoint stars; a rich edge has five. Four is forbidden.
Sources
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
  - Introduction; Proposition 2.1; references to Jaeger (1985, 1988) →
  - Theorem 1.1; Section 3; Appendix A →
Open statement page →

Counterexamples 2

Related advances 1

Proved
Infinitely many Petersen-coloring counterexamples
Corollary 5.1 combines the finite counterexample with the universal-target theorem of Ma, Mattiolo, Steffen and Wolf.
Putman 2026
Theorem · Related result
ProvedPutman 2026
Infinitely many Petersen-coloring counterexamples
Infinitely many connected simple bridgeless cubic graphs admit no Petersen coloring.
Assumptions
- Corollary 5.1 combines the finite counterexample with the universal-target theorem of Ma, Mattiolo, Steffen and Wolf.
In this problem
Corollary 5.1 combines the finite counterexample with the universal-target theorem of Ma, Mattiolo, Steffen and Wolf.
Sources
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
Open statement page →

Supporting results 1

Proved
Petersen and normal-five colorings are equivalent
The paper gives an explicit bijection using P = KG(5,2).
Putman 2026
Equivalence · Supporting result
ProvedPutman 2026
Petersen and normal-five colorings are equivalent
For each finite loopless cubic multigraph, the existence of a Petersen coloring is equivalent to the existence of a normal five-edge-coloring.
Assumptions
- The paper gives an explicit bijection using P = KG(5,2). Bridgelessness is not needed for this equivalence.
In this problem
The paper gives an explicit bijection using P = KG(5,2). Bridgelessness is not needed for this equivalence.
Sources
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
Open statement page →

Constructions · 2

Inspect the main graph

Explore this construction in the Landscape ↑

Order and size: 112 vertices; 168 edges
Coloring encodings: Petersen: 3,640 variables and 68,324 clauses; normal five: 1,960 variables and 25,484 clauses
Certificate tools: CaDiCaL 3.0.1 at c60730422e758ef1cebe7aeddf2dda31c996bf04; drat-trim at 2e3b2dc0ecf938addbd779d42877b6ed69d9a985
Normalized edge-list SHA-256: dc16cc18600cf77c8661b7baf89c7019f265299308541961ff884ea7187b4e8b

The exact adjacency data identifies this witness. Inspecting neighbors does not verify noncolorability, and 112 is not asserted to be minimal.

The main 112-vertex counterexample →

Inspect the symmetric graph

Explore this construction in the Landscape ↑

Order and size: 112 vertices; 168 edges
Coloring encodings: Petersen: 3,640 variables and 68,324 clauses; normal five: 1,960 variables and 25,484 clauses
Certificate tools: CaDiCaL 3.0.1 at c60730422e758ef1cebe7aeddf2dda31c996bf04; drat-trim at 2e3b2dc0ecf938addbd779d42877b6ed69d9a985
Normalized edge-list SHA-256: 0f2d8858110c6f012de7ddffa92fdbc709d7da630f199b0e3c81bb56eb6b35c7

The exact adjacency data identifies this witness. Inspecting neighbors does not verify noncolorability, and 112 is not asserted to be minimal.

A distinct symmetric 112-vertex counterexample →

Connections

Equivalent formulations 1

Every bridgeless cubic graph admits a Petersen coloring equivalent to Normal five-edge-colorings for bridgeless cubic graphs.
Cited equivalence
Jaeger’s theorem gives equivalent existence conditions for each loopless cubic graph.
Limit The positive universal assertions are both refuted by the reported witness; equivalence remains a valid theorem.
Sources & review
Relationship statement: Petersen and normal-five colorings are equivalentProved
Independent relationship review: not recorded. Link to this connection

Consequences 1

Assuming The main 112-vertex counterexampleProved

A finite obstruction has an infinite-family consequence
Under stated assumptions
The universal-target theorem cited in Corollary 5.1 turns the finite counterexample into an infinitude result for connected simple bridgeless cubic graphs.
Limit This consequence does not assert that the witnesses refute weaker cycle-cover or flow conjectures.
- Infinitely many Petersen-coloring counterexamplesProved
Sources & review
Supporting statements
- Infinitely many Petersen-coloring counterexamples →
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture ↗Corollary 5.1; Ma–Mattiolo–Steffen–Wolf (2025)
Source-grounded explanation · independent explanation review: pending.

Approaches

How the problem is attacked, and what each line of attack cannot yet reach.

Build the obstruction from small pieces

Delete the endpoints of one Petersen edge to obtain the eight-vertex four-pole F. Join four copies of F and a four-vertex claw six-pole C into a 36-vertex four-pole L, then join three L copies and another C into G. The source specifies every semiedge join.

Cannot yet reach Copy counts do not specify the graph without the precise joins and labeling map.

The main 112-vertex counterexample (Proved)

Sources & review

Supporting statements

The main 112-vertex counterexample →

A 112-Vertex Counterexample to the Petersen Coloring Conjecture ↗Theorem 1.1; Section 3; Appendix A

Source-grounded explanation · independent explanation review: pending.

Timeline

Aug 8, 2026Two explicit counterexamples and certificatesRelated result
Putman publishes the graph constructions, encodings and external checks; the frozen release is version 1.1.0.
This is a selected source-supported milestone, not an exhaustive history.
- The main 112-vertex counterexampleProved
- A distinct symmetric 112-vertex counterexampleProved
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture ↗Theorem 1.1; Section 3; Appendix A
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture ↗Theorem 6.1; Section 6
- Petersen counterexample: frozen construction and certificates ↗03_CERTIFICATION, 04_OPTIONAL_D3 and 05_DOCUMENTATION
Also on the Frontier: Petersen coloring conjecture
1988Jaeger’s coloring questionFoundation
The selected paper attributes the bridgeless cubic question to Jaeger’s 1988 chapter.
This is a selected source-supported milestone, not an exhaustive history.
- Every bridgeless cubic graph admits a Petersen coloringDisproved
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture ↗Introduction; Proposition 2.1; references to Jaeger (1985, 1988)
1985The normal-five formulationFoundation
Jaeger’s earlier work establishes the coloring equivalence recalled in Proposition 2.1.
This is a selected source-supported milestone, not an exhaustive history.
- Petersen and normal-five colorings are equivalentProved
- A 112-Vertex Counterexample to the Petersen Coloring Conjecture ↗Introduction; Proposition 2.1; references to Jaeger (1985, 1988)

Full history with sources →

Evidence

Evidence by kind
Literature	1 preprint · 1 project Status OpenMath assessment · Oct 14, 2026. Disproved: A 112-Vertex Counterexample to the Petersen Coloring Conjecture · Counterexample reported with checked SAT certificates ↗ · source dated Aug 8, 2026 · checked Oct 14, 2026Universal Petersen coloring assertion; minimum counterexample order is not determined.
Formal	None linked Reported in sources: SAT/DRAT certificates are available in the immutable archive. They are computational proof evidence, not an identified Lean or Isabelle theorem; OpenMath has not executed the certificates.
Computation	2 explicit witnesses Inspect the main graph Inspect the symmetric graph
Review	Not yet reviewed OpenMath assessment: A source-reported 112-vertex counterexample refutes the universal coloring conjecture. A second nonisomorphic witness is separately certified; neither establishes the smallest possible order. Source comparison and presentation; independent mathematical review remains pending. OpenMath pilot collection · OpenMath source curation · assessed Oct 14, 2026 · review due Jan 14, 2027 Collection last checked Oct 14, 2026.

Sources

Choose a starting point below. Each result links to its exact statement, cited passages and checks.

Start here

Original question
A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
Read the coloring definition and Jaeger equivalence.
Proof source
A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
Read the main construction and exact labeled graph.
Proof source
Petersen counterexample: frozen construction and certificates →
Inspect the encodings, certificate manifests, logs and reproduction instructions.

Bibliography 2

A 112-Vertex Counterexample to the Petersen Coloring Conjecture →
Bryce Putman · Preprint · Aug 8, 2026
Theorems 1.1 and 6.1, Proposition 2.1, Corollary 5.1, Appendices A–B and computational provenance.
Petersen counterexample: frozen construction and certificates →
Bryce Putman · Project documentation · Aug 8, 2026
Version 1.1.0; exact graphs, encoders, manifests, logs and separate DRAT proof files.

Selected literature; source observations and coverage limits are retained in the publication details.

Contributors

François Jaeger posed the coloring question and established its normal-five formulation. Bryce Putman authored the 2026 construction and verification release, reporting extensive OpenAI-model assistance and accepting responsibility for the final work. CaDiCaL and drat-trim supply distinct solver and certificate-checking roles. Ma, Mattiolo, Steffen and Wolf supplied the theorem used for the infinitude consequence.

Authors & roles

A 112-Vertex Counterexample to the Petersen Coloring Conjecture →

Bryce Putman

Putman reports extensive OpenAI-model assistance in discovery, search, verification and preparation; he reviewed the final claims and artifacts and accepts responsibility.

Petersen counterexample: frozen construction and certificates →

Bryce Putman

The author attributes discovery and verification assistance to OpenAI systems; source logs are external computational reports.

These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.

Record details

Record version: 1
Classification: MSC2020 05C15 / 05C21
Prerequisite level: undergraduate

Independent mathematical review is pending. External certificates and manuscript proofs are attributed to their sources.

Source observations & version history →

Overview

Known

Related open questions

Latest

Definitions

Landscape

The 112-vertex counterexample

Check the witness

From the Petersen graph to the obstruction

The main 112-vertex counterexample

Inspect the main graph

Inspect the exact adjacency

Inspect the symmetric graph

Inspect the exact adjacency

Results

The question 1

Assumptions

In this problem

Sources

Equivalent formulations 1

Assumptions

In this problem

Sources

Counterexamples 2

Assumptions

In this problem

Proof outline

Sources

Assumptions

In this problem

Sources

Related advances 1

Assumptions

In this problem

Sources

Supporting results 1

Assumptions

In this problem

Sources

Inspect the main graph

Inspect the symmetric graph

Connections

Equivalent formulations 1

Consequences 1

Related problems

Approaches

Build the obstruction from small pieces

Timeline

Evidence

Sources

Start here

Bibliography 2

Contributors

A 112-Vertex Counterexample to the Petersen Coloring Conjecture →

Petersen counterexample: frozen construction and certificates →