ProbXiv
sign in
Problem archiveProblem record

Asymptotically attaining the Moore bound

Combinatorics · posed by Béla Bollobás, 1978 · solved

2 comments

Statement

For positive integers dd and kk, let nk(d)n_k(d) be the maximum order of a graph of maximum degree at most dd and diameter at most kk. It is shown that lim⁡d→∞nk(d)dk=1\lim_{d \to \infty}\frac{n_k(d)}{d^k} = 1 for every fixed kk, thereby resolving the asymptotic degree-diameter problem for fixed diameter.

Also proved a similar lower bound on the edge-variant of the problem, and a tight asymptotic for the bipartite variant of the edge problem.

Record

Source
Added
Links

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. construction · #1

    Wouter Cames van Batenburg and Samuel Korsky, using GPT-5.6

    That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.

    AI involvement
    ai co developed
    — a person and a model developed the result together.

    The paper's tool disclosure states that GPT-5.6 Pro, used in exploratory brainstorming directed by the authors, suggested splitting complete flags into their odd- and even-rank subflags. That suggestion arose in connection with the edge problem but became the halved-flag construction carrying Theorem 1.1 itself, the graph being named for it. The authors developed it, formulated and verified every argument, and take full responsibility. Generative AI also assisted the Lean 4 formalization.

  2. Machine-checked by Lean on #1 · not a person

    lean: correctLean

    scope Lean formalization of the result

    Lean 4 formalization at github.com/woutercvb/wewantmoore, checked by the site on 2026-08-06 at commit 32beb227. DegreeDiameter.theorem_1_1 states Theorem 1.1 itself, as a limit of nKD k d / d^k, and corollary_1_2 states Corollary 1.2; neither is a weakened lemma, and a second independent route is proved alongside each under _via_big_cell. No sorry or admit appears in the sources, and the committed axiom audit shows both final theorems resting only on propext, Classical.choice and Quot.sound. That audit is not taken on trust: the repository's CI builds the project from the pinned toolchain and manifest, regenerates the axiom and dependency reports, and fails if they differ from the committed ones. It passes on this commit. The formalization was itself AI-assisted, per the paper's disclosure, and the authors note it is not a line-by-line transcription: k = 1 is handled by the same construction rather than by complete graphs, and the order and cap asymptotics go through leading terms rather than the displayed O_k(q^-1) estimates.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.