The most common degree sequence of a labelled graph
Abstract
Draw a graph on the labelled vertex set {1,…,n} uniformly at random — equivalently, sample the Erdős–Rényi model G(n,1/2) — and record the multiset of its vertex degrees. Which multiset is the most likely one? Ekhad and Zeilberger asked and answered the corresponding question for round-robin tournaments up to n=15, continuing a programme of MacMahon; for graphs we could not find the question asked anywhere, and its natural guess is wrong. We determine, for every n ≤ 12, the exact maximum of N(d), the number of labelled graphs whose degree sequence is d, together with the complete set of maximisers. At n=9, for instance, the unique maximiser is (6,5,5,4,4,4,3,3,2) with 941 371 200 realisations, while the 4-regular sequence — the naive answer — has only 1 024 380, smaller by a factor of about 919. Over the computed range the maximiser set has one, two or three elements and is always closed under d ↦ (n-1)-d. We determine, for the same range, the exact number of labelled graphs whose maximum degree is attained by a single vertex: the finite counterpart of the result of Erdős and Wilson that almost all graphs have such a vertex. Both are contrasted with the degree-vector question, whose answer is a (near-)regular sequence and whose asymptotic form is known. The method is a dynamic program that seats one vertex at a time and carries only the sorted multiset of the degrees so far; its state space is the set of realisable degree sequences (222 117 of them at n=12) rather than the 2⁶⁶ graphs. Every result stated here is machine-checked in Lean 4.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
eefea0aeee86c1c54d0d0c6c235a4d904b15728185606ac8d4566a4cfcd50656
Claim ledger
Stated results
DS1routine2026-08-28
The bridge: the labelled graphs on Fin n are exactly the codes tours Gr n, their degree lists are scores, gdeg is Mathlib's SimpleGraph.degree, and there are 2^C(n,2) of them
DS2routine2026-08-28
N(d) is the dynamic program's cell, and under the key certificate bestW is the maximum of N over ALL degree sequences with modeKeys the exact set of maximisers
DS3routine2026-08-28
The degree-sequence tables of labelled graphs on n <= 12 vertices: total weight, number of realisable sequences, modal value and modal keys, the vecW maximum and its keys, the unique-maximum-degree count, and the key certificate – one native_decide per n
DS4routine2026-08-28
The number of labelled graphs whose maximum degree is attained by exactly one vertex is the table's uniqueOfTbl
DS5routine2026-08-28
The number of k-regular labelled graphs on n vertices is the table's cell at the constant degree sequence – the one case where the degree-VECTOR and degree-MULTISET questions coincide exactly
DS6candidate2026-08-28
The modal degree sequence of a labelled graph on n vertices, for n <= 12: the maximum of N over all degree sequences, the sequences attaining it, and the proof that there are no others
DS7candidate2026-08-28
The number of labelled graphs on n vertices whose maximum degree is attained by a unique vertex, for n <= 12
DS8known data2026-08-28
The number of realisable degree sequences on n <= 12 vertices, as a proved count of PAIRWISE DISTINCT sequences whose N is nonzero – OEIS A004251
DS9known data2026-08-28
The number of k-regular labelled graphs on n <= 12 vertices, every k – the rows of OEIS A059441
DS10routine2026-08-28
k-regular labelled graphs in graph language: the count is a cell of the table, and there are none once k >= n
DS11known data2026-08-28
The maximum, over CONSTANT degree vectors, of the number of labelled graphs realising them, for n <= 12, and the degrees attaining it
DS12routine2026-08-28
Negative controls: brute-force N(d) over all 2^C(n,2) graphs at n <= 4; the mode value at n = 9 is neither larger nor smaller; the modal sequence is NOT the regular one; the mode is not always unique; non-graphical sequences get N = 0; the key certificate is neither vacuous nor unsatisfiable; GraphFin is the labelled graphs and nothing more
DS13measurement2026-08-28
Cost and reach: n = 13 measured outside Lean; the Lean frontier is n = 12 at 297 CPU-seconds and 7.5 GB; and hoisting a table-wide maximum out of a filter predicate is worth 86x (358 s vs 4.15 s – the 90x round-up standardised to the measured pair 2026-08-28) on this workload
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Which degree sequence do the most labelled graphs have? — and how often does the maximum degree belong to a single vertex? Both answered exactly, in Lean, for every n ≤ 12.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7