Version 1.1.0; exact graphs, encoders, manifests, logs and separate DRAT proof files.
Source-reported results and external checks are separate from independent OpenMath assessment.
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
CaDiCaL 3.0.1 reports UNSAT; drat-trim reports VERIFIED for four DRAT proofs. Separate encoders, satisfiable controls and status-parsing negative controls support the reported checks.
Passage ID: petersen-coloring:entry:certificates:v1
Source item: certificates
Source record: petersen-coloring:source:archive:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v7
Source assessment
Proved
External SAT and DRAT checks reported
Four graph/formulation pairs; not an OpenMath execution.
Source date Aug 8, 2026 · Observed Oct 14, 2026
Construction
Inspect the main graph
Proof explanation
Two independent coloring encodings
Source assessment
Proved
External SAT and DRAT checks reported
Four graph/formulation pairs; not an OpenMath execution.
Source date Aug 8, 2026 · Observed Oct 14, 2026
Construction
Inspect the symmetric graph
History
Two explicit counterexamples and certificates
Question
Petersen coloring conjecture
Further reading
Inspect the encodings, certificate manifests, logs and reproduction instructions.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Dataset
No OpenMath execution recorded
Small archive inspected; exact graph data imported. SAT solving and DRAT certificate checking have not been rerun by OpenMath.
Resource revision: 1.1.0
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
75e935442fcb5457a9cfd0fd07c6d0a5b5fca80e1aeedab6e7243e8ccde9287bDataset
Source-reported evidence
The source reports successful drat-trim checks for both formulations of both graphs. These large certificate files were not executed by OpenMath.
Resource revision: 1.0.0 (unchanged certificate bytes in release 1.1.0)
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
8af3eec414b652f05c56979dc148321535cdc51ff9cbd59dff278ef3d53d9832Recorded authorship
Bryce Putman
The author attributes discovery and verification assistance to OpenAI systems; source logs are external computational reports.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
Petersen counterexample: frozen construction and certificates
Linked proof prose is not republished. Any copied graph data is CC0, as specified by its archive.
Source terms ↗