Formally verified AI-led

Six-task counterexample to the Kernel Conjecture of pinwheel scheduling

A six-task pinwheel scheduling instance with periods $(3, 4, 5, 20, 22, 36)$ can be scheduled, but not once its longest period is cut to 32, which refutes the Kernel Conjecture and the equivalent $2^k$ Conjecture of Gąsieniec, Smith and Wild.

Lab: Independent
Model: GPT-6 Astra (in OpenAI Codex)
Field: Computer science
Date: 2026-09-30
Problem posed: 2021 · open 5 yrs

Sources

Original work

GitHubMathIsEvenEasier/pinwheel-kernel-counterexample↗

What was found

In pinwheel scheduling one task is performed per day, and a task with period $a_i$ must be performed at least once in every $a_i$ consecutive days. Gąsieniec, Smith and Wild conjectured that every schedulable instance with $k$ tasks is dominated by a schedulable one, with no period longer, whose largest period is at most $2^{k-1}$ , and proved this equivalent to the claim that a loosely schedulable instance always has a schedule with a free day at least every $2^k$ days. For six tasks the cap is 32. A 36-day repeating word schedules $(3, 4, 5, 20, 22, 36)$ , while finite certificates show that $(3, 4, 5, 20, 22, b)$ cannot be scheduled for $b = 32$ or $b = 35$ , so the threshold for the sixth period is exactly 36 and every dominated instance capped at 32 fails by monotonicity. Each certificate lists every reachable state with a rank that strictly decreases along every legal move, which rules out non-periodic schedules too. The repository carries a Lean 4 formalization of the certificate argument and of both endpoints, built against the standard library alone.

Novelty check

Read Conjectures 2.2 and 2.3 and Proposition 2.4 of arXiv:2111.01784 (Gąsieniec, Smith and Wild, 2021; ALENEX 2022) on 2026-10-06 and confirmed that the instance contradicts them as stated, domination meaning componentwise at most. Web searches for the Kernel Conjecture and the $2^k$ Conjecture, and an arXiv title scan of pinwheel scheduling papers from 2024 to 2026, found no earlier counterexample or resolution; the 2026 papers on pinwheel density thresholds address, by their titles, a different conjecture. That is not a systematic review of the scheduling literature.

Caveats and known objections

No paper and no peer review: the evidence is a GitHub repository holding the certificates, a Python checker and a Lean development, all produced by the workflow that found the example. The human who directed it is not named. The repository credits the model with discovering the example, writing the searches, certificates and checker, and developing the formalization, and the human with setting the objective, supervising, and asking for the prior-work and formal checks, which is why autonomy is ai-led rather than autonomous. The Lean build was run by the authors on a cloud worker and replayed through the Nanoda kernel, also by the authors; nobody outside has compiled it or audited that the Lean statements match the conjecture. Graded formal because the finite claim is exactly rerunnable, and this registry reran it with separate code. The result bounds any universal six-task cap from below by 36; it does not show that 36 suffices.

Independent checks

whataifound.org (independent recomputation, Python): Wrote a feasibility search sharing no code with the repository. From the all-zero age vector, $(3, 4, 5, 20, 22, 32)$ and $(3, 4, 5, 20, 22, 35)$ reach 50,881 and 56,284 states, the counts the two certificates report, and in both every walk dies out once dead ends are pruned; $(3, 4, 5, 20, 22, 36)$ keeps an infinite walk, and the repository's 36-day witness word meets every period. This checks the finite claim, not the Lean development.

Nanoda kernel replay (author-run, reports public): Replayed the four endpoint theorems and their dependencies, 6,850 declarations, on 2026-10-01, admitting only propext and Quot.sound. · link ↗

Also recorded at

vibemathedthe-pinwheel-kernel-conjecture-a-six-task-counterexample

Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-10-06AddedEntered the registry graded Formally verified and AI-led.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Graded formally verified for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Six-task counterexample to the Kernel Conjecture of pinwheel scheduling. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-30-pinwheel-kernel-conjecture

BibTeX

@misc{whataifound-independent-2026-conjecture,
  title        = {Six-task counterexample to the Kernel Conjecture of pinwheel scheduling},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-09-30-pinwheel-kernel-conjecture}
}

Related findings

Formally verifiedA prescribed Hamiltonian cycle that a book-embedding algorithm cannot produceIndependent · 2026-08-11 Formally verifiedLean disproof of Krempa's matrix form of the Koethe conjectureOpenAI / Epoch AI · 2026-09-03 Formally verifiedUnrestricted Boolean multiplicative complexity of four-term binary polynomial multiplicationIndependent · 2026-08-31

scheduling algorithms counterexample lean formalization construction

← All computer science findings in the registry