The Pinwheel Kernel Conjecture: a six-task counterexample
A pinwheel instance is a sorted tuple of positive integers . A feasible schedule performs one task per integer time slot, with task appearing in every block of consecutive slots. The Kernel Conjecture asks whether every feasible dominates a feasible sorted instance with for every and (Conjecture 2.3 of Gąsieniec, Smith and Wild).
- Result
- Disproved(see note)
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Computation
- Field
- Pinwheel scheduling; finite-state verification
- Posed by
- Leszek Gąsieniec, Benjamin Smith and Sebastian Wild, Towards the 5/6-Density Conjecture of Pinwheel Scheduling, Conjecture 2.3 (2021 preprint; ALENEX 2022).
- Year posed
- 2021
- Years open
- 5y
- Solved
- 2026-09-30
- Model
- OpenAI Codex (GPT-6 Astra)
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Site-confirmed
- Publication
- Announced
- Significance
- 12 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The instance is feasible, but is not. More strongly, is feasible exactly when .
A 36-slot periodic witness proves feasibility. A forward-closed certificate for period 35 has 56,284 states and 107,847 legal transitions, with a natural-number rank decreasing at every step. This excludes all infinite schedules, including nonperiodic ones. Monotonicity rules out every dominated six-task instance with all periods at most , refuting the original Kernel Conjecture. A separate certificate checks period 32.
The result shows that any universal six-task cap must be at least 36, not that 36 suffices universally. In practice, truncating deadlines to 32 can turn a schedulable input into an infeasible one: this preprocessing rule is unsound. The example also supplies a certified regression test for scheduling solvers.
What the AI did
Under human direction, Codex selected and investigated the conjecture, implemented finite-state searches, found the counterexample, sharpened the sixth-period threshold to 36, generated finite certificates, wrote a separate Python checker, and developed the Lean formalization from the infinite-schedule definition to the final theorem. The human set the research objective, supervised the workflow, requested prior-work searches and formal verification, and required review before publication. No independent human mathematical verification is claimed.
Verification
Re-checked by this site on 4 October 2026 with an independent checker written from scratch (reachable age-state search with dead-state pruning, not the repository's code): (3,4,5,20,22,b) is infeasible for b = 30 to 35 and feasible for b >= 36, with state counts equal to the repository's (50,881 at b = 32, 56,284 at b = 35). The repository's check_counterexample.py also passed. The Lean development (260 modules, core Lean only, Lean 4.34.1) was searched and has no sorry, admit, axiom declarations, native_decide, opaque or unsafe; its log records only propext and Quot.sound. The site did not rebuild it, and the repository has no CI; the Azure and Nanoda logs are the author's. Statement fidelity to Conjecture 2.3 was checked by hand: ScheduleOK quantifies over all infinite schedules, and the formal claim drops sortedness, which makes it slightly stronger.
Sources
Submitted by ZestyRaven517 on