An eight-vertex candidate counterexample to OPG-500

Proved

OPG500Counterexample.eight_vertex_counterexample

by hao jia · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsformalizationgeodesicsgraph-theory

Let $H$ be the fixed graph on vertices $0,\ldots,7$ with edge set

\{01,02,03,04,05,06,12,13,14,15,17,23,24,26,27,35,36,37\}.

The target asserts that $H$ is 3-connected and that

\forall \ell:E(H)\to\mathbb R,\quad (\forall e,\ 0<\ell(e))\Longrightarrow \exists C,\quad C\text{ is an $\ell$-geodesic simple cycle and is not peripheral}.

The cycle may depend on the weighting, and tied shortest paths are included. This is an open formal target: the candidate repository and finite computations are not themselves a proof.

Preamble

import Definitions.Def_opg500_eight_vertex_graph

Formal statement

namespace OPG500Counterexample

/-- The fixed eight-vertex graph is 3-connected and, for every strictly positive
real edge weighting, has a vertex-geodesic simple cycle that is not peripheral. -/
theorem eight_vertex_counterexample :
    IsThreeConnected H ∧
      ∀ ℓ : EdgeWeight H, IsPositive ℓ →
        ∃ C : Cycle H, C.IsGeodesic ℓ ∧ ¬ C.IsPeripheral := by sorry

end OPG500Counterexample

Source

Target source: Open Problem Garden OPG-500, https://www.openproblemgarden.org/op/geodesic_cycles_and_tuttes_theorem, with the proposed fixed obstruction in candidate C10: https://github.com/vibemathing/problem-opg-500-geodesic-cycles/blob/a41fe59b4535851ea55f6e868e938b9aaf81e924/research/artifacts/candidates/opg500-a01-c10/tight-rank.md

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

For the graph $H$ on vertices $0,\ldots,7$ with edge set $\{\{0,1\},\{0,2\},\{0,3\},\{0,4\},\{0,5\},\{0,6\},\{1,2\},\{1,3\},\{1,4\},\{1,5\},\{1,7\},\{2,3\},\{2,4\},\{2,6\},\{2,7\},\{3,5\},\{3,6\},\{3,7\}\}$ , the graph has at least four vertices and deleting any set of fewer than three vertices leaves a connected induced graph. Furthermore, for every assignment of a strictly positive real weight to each edge of $H$ , there exists a cycle $C$ of $H$ such that, between every two vertices occurring in $C$ , some globally shortest simple path uses only edges of $C$ , while $C$ is not both chordless and surrounded by a connected-or-empty outside induced graph.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph