Pinwheel scheduling is the problem of arranging recurring tasks in a sequence with at most one task performed in each time slot. An instance consists of positive
integers 
.
Task 
must occur at least once in every block of 
consecutive slots. An instance is feasible if an infinite
schedule satisfies all these requirements. For example, the instance 
is feasible by alternating the two tasks.
The density of an instance is
 |
(1)
|
Feasibility requires 
, but this condition is not sufficient. The 5/6-density
conjecture asserts that every instance with 
is feasible (Gąsieniec et al. 2021).
The kernel conjecture for pinwheel scheduling (Gąsieniec et al. 2021) asserts that every feasible instance with 
has a feasible instance 
with 
for every 
and 
. MathIsEvenEasier (2026) reported a counterexample
using six tasks. In the family
 |
(2)
|
the instance 
is feasible exactly when 
. For 
, repeating the 36-slot word
 |
(3)
|
where the letters A through F denote the six tasks in order, gives a feasible schedule. The longest cyclic gaps between occurrences of these tasks are respectively 3, 4, 5, 20, 22, and 36.
The infeasibility of 
contradicts the proposed bound 
. Indeed, a feasible instance
whose requirements are all at least as strict as those of 
would also make 
feasible. The certificate for 
uses a finite directed
graph of 56,284 scheduling states and 107,847 legal transitions. The certificate
for 
has 50,881 states and 97,140 transitions. Each has a decreasing integer
rank on every transition. This rules out infinite schedules as well as periodic
sequences.
The same example refutes the related holiday conjecture that every 
-task
instance admitting a schedule with empty slots admits one with an empty slot in every
block of 
slots. Removing F from the schedule above gives such a five-task instance. If it
had an empty slot in every block of 32 slots, filling those slots with F would make
feasible. This counterexample does not settle
the 5/6-density conjecture.
The project reports human-directed proof discovery and Lean formalization by OpenAI Codex using GPT-6 Astra. As of Oct. 5, 2026, recorded Lean builds and an independent kernel replay checked the formal development, and VibeMathed had reproduced the finite state counts. Independent specialist review of the full argument had not been reported (MathIsEvenEasier 2026, VibeMathed 2026).
