---

A proof claim submitted on 2026-09-24 to the site's proof-claim tab of Problem 1016 by the account KNT, with a write-up and a Lean 4 development in the repository JWKNT/erdos1016 (its commit of 2026-10-03, pinned in the links). The write-up's author line reads KNT, which names the claimant; the tab credits GPT-6 Astra, and its notes say the proof was achieved via GPT-6 Astra, that is GPT-6 Pro under the name Astra in the web application. The site states that a listing on the tab is no guarantee of correctness and does not mean that anyone associated with the site has examined any part of the proof.

Submission note. Posted to erdosproblems.com as a proof claim by KNT (account KNT) on 24 September 2026, giving "GPT-6 Astra" as the AI used:

We prove this by tracking how efficiently a graph can realize an entire interval of cycle lengths, not just the number of cycles. Let Φ(R) measure the best normalized length coverage at cycle rank R or more. We show a near-halving recurrence: Φ(2^{CR⁴}) ≤ (1/2 + 1/R)·Φ(R) + 2^{2−R}. The deviations from exact halving are summable, so after j levels the coverage is O(2^{−j}). Reaching rank r takes log* r + O(1) levels, and this gives the log* n term. The recurrence comes from a statement about random edge sets: in a graph of huge cycle rank, remove a small subgraph with few components, such as one chosen cycle of each short length; then a uniformly random even edge set, restricted to the rest, is a union of disjoint paths with probability at most 1/2 + 1/R. A cycle that crosses between the removed subgraph and the rest splits into disjoint paths on each side, so this probability limits how many new cycle lengths the rest of the graph can contribute. Notes: This proof was achieved via GPT-6 Astra. Transparently: the process was to have an instance of GPT-6 Pro (Astra in the web app) generate a research prompt for another GPT-6 Pro session, which would in turn create a research.zip bundle of its findings, which would then get fed back into the first Astra session for another prompt, etc. The final proof was achieved on Session 111, but tens of thousands of supplementary lemmas and theorems (mostly all useless) were derived along the way. Sessions 31, 54, 55, and 107 were all long-horizon multi-agent attacks, the first three being ~5 hours each and the last being roughly 18 hours. We also have a full lean formalization of 494 files and about 83000 lines, passing certificate: (https://github.com/JWKNT/erdos1016/actions/runs/36026578423). Each major statement in the paper has a link to its corresponding lean formalization. This whole process took about 11 days.

The claim. Theorem 1.1 of the write-up (The minimum number of edges in a pancyclic graph, 9 pages, dated September 2026): there is an absolute constant $A$ such that for every $n\ge3$

$$\log_2n+\log_*n-A\ \le\ h(n)\ \le\ \lfloor\log_2n\rfloor+\log_*n+1,$$

where $n+h(n)$ is the least number of edges of a pancyclic simple graph on $n$ vertices and $\log_*x$ is the least $j\ge0$ such that $j$ applications of $\log_2$ take $x$ to a value at most one; in particular $h(n)=\log_2n+\log_*n+O(1)$. The lower bound is the problem's displayed question, answered yes, and with it the weaker statement $h(n)-\log_2n\to\infty$ that Erdős could not prove; the upper bound is Bondy's claimed bound with an explicit constant, proved by the write-up's own chord construction (Proposition 5.1), so the claim also settles the order of $h(n)$ and leaves no part of the problem open. The write-up's method, in this page's words from its abstract and introduction: its forest estimate (Theorem 1.2) concerns a connected graph of large cycle rank $r$ from which a union of cycles with at most $\sqrt r$ edges and at most $(\log_2r)/100$ components has been removed, and bounds by $1/2+20/\log^{(3)}r$ the probability that a uniformly random even edge set of the whole graph, restricted to the edges outside the removed cycles, is a forest; since a cycle meeting both the removed cycles and the remainder breaks into paths inside each, that bound caps the number of further cycle lengths the remainder can add, and this caps a normalized cycle-length capacity by a near-halving recurrence whose iteration produces the $\log_*n$ term. The upper bound takes an $n$-cycle, an arc cut into segments of lengths $2^i+1$ with their shortcuts, and $\log_*k-1$ further chords.

The postings. The tab entry of 2026-09-24 linked a write-up of about 40 pages and a formalization of 494 files, with the continuous-integration run of 2026-09-24 that certified the repository's first commit (the first record link); the author's comment of 2026-09-26 on the same entry announces a shorter proof, the 6-page body linked above, with a formalization of 247 files and about 41,000 lines, and says that the earlier paper and development are archived under old/ in the repository, where the first preprint link reaches the first write-up at the pinned commit; the README adds that the active build and the current certificate exclude that material. The shorter write-up names the commit of 2026-09-25 it describes and the continuous-integration run that certifies that commit (the second record link). The later preprint and formalization links pin the commit of 2026-10-03; no certificate run for that commit is linked, and the runs linked certify only the two earlier commits.

The formalization. At the pinned commit, Erdos1016/Main.lean proves Erdos1016.mainTheorem : Problem1016.MainTheorem and the equivalent mainTheorem_integer_excess: real constants $A_-$ and $A_+$ with $\log_2n+\log_*n-A_-\le h(n)\le\log_2n+\log_*n+A_+$ for every $n\ge3$, where $h(n)$ is defined, in the repository's CommunityStatement namespace, as the least number of edges of a SimpleGraph (Fin n) having a cycle of every length from $3$ to $n$, minus $n$, and $\log_*n$ as the least $k$ with $n\le T(k)$ for the tower $T(0)=1$, $T(k+1)=2^{T(k)}$. The write-up's Section 1.2 and its README say that the build uses Lean v4.19.0 with a pinned Mathlib, that the repository's verifier rebuilds every active module, audits the statements and axioms and permits only propext, Classical.choice and Quot.sound, and that the certified commit passed. These are the claimant's statements; nothing was built, replayed or audited in this corpus, and the fidelity of the Lean statement to the site's question was not reviewed by this project.

Depends on. No page of this wiki. The lower bound argument is self-contained and the upper bound is the write-up's own construction; Bondy's claimed bounds and Griffin's proof of the weaker lower bound, recorded on the problem page, are context.

Standing. Claimed: the entry is pending on the site's tab, whose only comment is the author's own update; the site's label is unchanged (OPEN, page last edited 27 December 2025, accessed 2026-10-07); there is no refereed version, no outside review, and no check of the argument or build of the development was made in this corpus. Read depth: the write-up's abstract, Section 1, Section 5 and Appendix A; no proof step is checked. The problem's standing is claimed through this pending full claim.