Solver developers
Add this pair of instances to your regression tests: expect “feasible” for a bound of 36 and “infeasible” for 32. Capping the periods at 32 destroys a valid solution.
COUNTEREXAMPLE · 6 TASKS
Four days make the difference.
A schedule with periods 3, 4, 5, 20, 22, 36 exists. Reducing the last period to 32 makes every infinite schedule impossible.
01 / CHECK A SCHEDULE
36 days, then repeat
Loading schedule…
02 / WHY THE COUNTEREXAMPLE WORKS
A working schedule. No possible small kernel.
One task runs each day. Each number is the longest gap that task may have between runs. Follow four steps: inspect a working schedule, see why every schedule fails at 35, and use that fact to rule out every kernel capped at 32.
Loading the guided proof…
03 / RULE OUT EVERY SCHEDULE
Try to keep scheduling forever
Choose the next task. The rank is the largest number of legal steps still possible. Every legal move reduces it.
Loading 50,881 certificate states…
99
legal steps left
on the longest path
on the longest path
RUN A TASK
The initial state deliberately gives the scheduler an advantage: every age starts at zero, as if all six tasks had just run at once. Even from this state, no schedule lasts 100 steps. Idling cannot help: any idle day can be filled with task A.
97,140 transitions. Every one accounted for.
Check every legal move and decreasing rank in your browser.
WHY DO FIVE TASKS WORK, WHILE SIX CHANGE THE RESULT?
A feasible schedule need not leave regular free days
The first five tasks even admit this 14-day cycle:
A B C A D B A C A B E A C B
Its maximum gaps are 3, 4, 5, 14, 14 — all below the five-task bound of 16. Adding F requires a whole day for it at regular intervals. With periods 3, 4, 5, 20, 22 for A–E, this is possible every 36 days, but not in every 35-day window.
Is this about average utilization?
Average utilization alone is not enough. With a period of 32 for F, the sum of the required frequencies is about 91%, yet no schedule exists. The placement of tasks and their deadlines also matters. The exact threshold of 36 is established by the full certificate checked in Lean; we have not derived a separate short proof of this number.
04 / PRACTICAL USE
A regression test for an unsound reduction
Recurring inspections
Imagine one service station and six inspections. Inspection F fits if its gap may be up to 36 days. Requiring it at least once every 32 days conflicts with the other deadlines.
Algorithm audits
A small, separate verifier checks the result without repeating the search. The Lean formalization also checks the mathematical argument from the model to the conclusion.
Model assumptions: each task takes exactly one time slot, one task runs at a time, and periods are integers. Breaks, travel time, and unequal task durations require a different model. This is a correctness test, not a production scheduling system.
What has been checked?
Lean 4.34.1: PASS in Azure · 260 modules · exact threshold 36. Axiom audit: only propext and Quot.sound. A deliberately corrupted rank was rejected. Nanoda: PASS · 6,850 declarations · only propext and Quot.sound · a corrupted proof control was rejected. The separate Python checker also passed.
Conjecture 2.3, ALENEX 2022 · Certificate data · Download the proof, Python checker, and Lean sources
Priority has not been established. This site is for exploration; the download contains the full proof and describes its trust assumptions.
The 2k Conjecture also fails
Conjecture 2.2 says that every loosely schedulable k-task instance has a schedule with a holiday at least every 2k days. A holiday is a day on which no task runs. Proposition 2.4 makes this conjecture equivalent to the Kernel Conjecture.
Our example gives a direct explanation. Remove task 6 from the working 36-day schedule: the remaining five tasks (3,4,5,20,22) have a valid periodic schedule with holidays. If those five tasks admitted a schedule with a holiday in every 32-day window, we could fill every holiday with task 6. That would solve (3,4,5,20,22,32), which the certificate excludes. Thus the five-task instance refutes the 25 = 32 holiday bound.
This consequence follows from the existing witness and certificate. It is not a separately formalized Lean endpoint.
Acknowledgments
This work was inspired by Dr. Samuel Allen Alexander’s YouTube channel, @xamualexander. Still there.