An affirmative example for the k=4 case of Kourovka Problem 20.71

Author: Jitendra Prajapati (IIT Madras).

Paper: Read the PDF · Download the PDF · LaTeX source.

Contact via GitHub (@infinityscroll). The verification scripts were prepared with assistance from AI system, under the author's direction; the witness and all counts were additionally re-verified by independent brute-force computation, and the central claim is machine-checked in Lean 4 (see INDEPENDENT_VERIFICATION.md).

Problem 20.71 on printed page 154 in the 21st edition (July 3, 2026 update) of the Kourovka Notebook asks, for k = 2, 3, 4, whether a connected graph having k isomorphism types among its vertex-deleted cards can have more than k vertex-orbits under its automorphism group.

The source snapshot is

Official Kourovka Notebook No. 21, July 3, 2026 update
https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/07/21tkt.pdf
Problem 20.71: printed page 154 (zero-based PDF page index 153)
1740593 bytes
SHA-256 301b0cdcc53abc88b57cc0732cad73bf8fbe1c9ba0de5a0a794070398e3395fe
HTTP Last-Modified: Fri, 03 Jul 2026 12:44:05 GMT

The graph below answers the k = 4 case affirmatively.

Let G have vertex set {0,1,...,8} and edge set

03 04 07 14 15 16 25 26 27 28 36 37 38 48 57 68.

Its graph6 representation is HCpbdgy. It is connected; for example,

03 04 07 14 15 16 25 28

is a spanning tree.

Color refinement, initialized by degree, stabilizes at

{0,5}, {1,4}, {2,3}, {6,8}, {7}.

Every automorphism preserves these cells. The permutation

(0 5)(1 4)(2 3)(6 8)

is an automorphism, so the five displayed cells are precisely the vertex orbits. (The exact verifier additionally enumerates all 9! permutations and finds only the identity and this involution.)

There are exactly four isomorphism types, with deletion vertices grouped as

{0,5}, {1,4}, {2,3,6,8}, {7}.

The involution above supplies the isomorphisms within each of the pairs {0,5}, {1,4}, {2,3}, and {6,8}. Explicit maps from G-2 to all other members of its card class (written as old-vertex maps) are

G-2 -> G-3: 0->5, 1->4, 3->2, 4->1, 5->0, 6->8, 7->7, 8->6
G-2 -> G-6: 0->2, 1->4, 3->7, 4->8, 5->1, 6->0, 7->5, 8->3
G-2 -> G-8: 0->3, 1->1, 3->7, 4->6, 5->4, 6->5, 7->0, 8->2

The four card types are distinct already by their degree multisets:

delete 0: 2,3,3,3,3,4,4,4
delete 1: 2,2,3,3,4,4,4,4
delete 2: 2,3,3,3,3,3,3,4
delete 7: 2,2,3,3,3,3,4,4.

Consequently G has four card types but five automorphism orbits.

This matches the quantifiers literally: the graph is finite, simple, undirected, and connected; "four types" is exactly four distinct card isomorphism classes (with multiplicities 2,2,4,1), not at most four. It settles the k=4 existence subcase only. It does not answer the k=2 or k=3 subcases.

The orbit and card calculations above form a short certificate independent of the discovery software: color refinement plus the displayed involution proves that there are exactly five vertex-orbits; the displayed deletion isomorphisms prove that there are at most four card types; and the four different degree multisets prove that there are at least four.

verify_kourovka_20_71_counterexample.py uses only the Python standard library as an exhaustive independent audit. It determines the automorphism group by checking all 9! permutations and canonically classifies every card by checking all 8! vertex orders.

Separate point checks agree:

• NetworkX 3.3 GraphMatcher finds two automorphisms and the same four card classes.

• nauty 2.9.3 dreadnaut reports group size 2 and five orbits, generated by (0 5)(1 4)(2 3)(6 8).

• nauty delptg -l gives the following canonical graph6 card codes, again yielding four types:

  GhEIXk  GCLZLS  GaIHjo  GaIHjo  GCLZLS  GhEIXk  GaIHjo  GR`?x[  GaIHjo
  

These checks establish the affirmative example itself; no minimality claim is needed for the answer to k=4.

Kourovka2071.lean gives a separate Lean 4 certificate. It defines the nine-vertex simple graph, proves it connected, exhaustively classifies all automorphisms and all vertex-deleted-card isomorphisms, and concludes with

theorem affirmative_k4 :
    ∃ G : SimpleGraph (Fin 9),
      G.Connected ∧ HasExactlyCardTypes G 4 ∧ HasExactlyVertexOrbits G 5

It compiles in the current formal-conjectures environment with

lake env lean Kourovka2071.lean

and contains no sorry, admit, added axiom, or unsafe declaration. Its finite exhaustive decisions use native_decide, so the certificate trusts Lean's native compiler in addition to the kernel.

The discovery search used geng and nauty certificates. A complete census of connected unlabeled graphs through eight vertices found no example; the graph above was the first graph6 hit at order nine. This minimal-order claim depends on that exhaustive software census and is separate from the elementary verification of the affirmative example itself.

The exact census command was

geng -cq N | python3 search_kourovka_20_71.py

using nauty 2.9.3 and pynauty 2.8.8.1. The checked connected-unlabeled graph counts were

N=1: 1       N=2: 1       N=3: 2       N=4: 6
N=5: 21      N=6: 112     N=7: 853     N=8: 11117.

A complete continuation through all 261080 connected graphs of order nine, using

geng -cq 9 | python3 search_kourovka_20_71.py --all-targets

found the displayed k=4 witness and no k=2 or k=3 witness at that order. That latter no-hit is computational evidence about the two remaining subcases, not a solution of them.

A faster two-stage pipeline (degfilter.c + stage2_k23.py; a graph with at most 3 card types has at most 3 distinct degrees, and card classes refine the (degree-multiset, triangle-count) card fingerprints) extends the negative census for the two remaining subcases:

• order 10: all 11,716,571 connected graphs — no k = 2 or k = 3 example;
• order 11: all 1,006,700,565 connected graphs — no k = 2 or k = 3 example.

So any graph with two (resp. three) card types and more than two (resp. three) automorphism orbits has at least 12 vertices.

A complete recount of k = 4 witnesses (stage2_k4.py, no degree filter) shows that order 9 admits exactly two such graphs: HCpbdgy and its complement HCZetxu (both connected; card types and orbit counts are complement-invariant). So the k = 4 example is unique up to complementation at minimum order. Curiously, no graph of order 10 is an example for any k in {2, 3, 4}.

A short note (LaTeX in note/) presents the k = 4 answer with a fully hand-checkable proof plus these census results. Exploratory sweeps beyond order 11 also found no witness in the tested connected slices (results_extended/, all with 0 witnesses):

• regular graphs of orders 12--14 with degrees 2 <= d <= (n-1)/2 (largest slice: 21,609,300 connected 6-regular graphs on 14 vertices);
• graphs of orders 12--13 with degrees in {a, a+1}, a = 2,...,5, covering 15,409,504 and 836,922,152 graphs respectively.

These slices are not exhaustive on their own. Although card types and orbit counts are complement-invariant, complementation need not preserve connectivity, so a connected-only generation cannot infer the untested complementary slices directly; the complementary slices are instead covered by testing disconnected unions (see results_extended/SUMMARY.md), since the complement of a disconnected graph is always connected.

Order 12 is fully resolved: a complete census of all 164,059,830,476 connected graphs on 12 vertices (matching OEIS A001349 exactly; 1,905,839,762 passed the degree filter, 32,500 required canonical labelling) found no k = 2 or k = 3 example. The unconditional bound: any example for the remaining subcases has at least 13 vertices.

The July 2026 Notebook still prints Problem 20.71 without a solution note, and the separate July update file does not mention it. The July 20, 2026 paper On Some Problems from the Kourovka Notebook solves eight other problems, not 20.71. Exact-statement searches of indexed web results, arXiv, GitHub, and MathNet found no matching solution.

The closest historical source located was Josef Lauri's 1997 survey Pseudosimilarity in Graphs---A Survey, which formulates the underlying partition-refinement question in terms of card-equivalence versus automorphism-equivalence classes. Its examples and constructions do not give the four-card-type/five-orbit graph above. Searches of the later pseudosimilarity literature, including the 2016 second edition of Lauri--Scapellato's Topics in Graph Automorphisms and Reconstruction, also found no such example.

The graph itself is known as an unannotated data item: the exact graph6 string HCpbdgy already occurs in generic Ramsey/critical-graph datasets in the GitHub repositories Steven-VO/circulant-Ramsey, gwen-mckinley/ramsey-books-wheels, and melvin-adekanye/Research. Those hits do not mention deletion cards, automorphism orbits, or Problem 20.71. Thus the graph must not be claimed as new; the potentially new item is this specific observation about it. The negative search still does not establish publication priority. The indexed-literature audit found no remaining concrete collision lead, but private correspondence and unindexed computations remain possible. The problem poser or the Kourovka editors should therefore confirm priority before an unqualified novelty claim is made.