Kyoto University Mathematician Proves 33-Year-Old Conjecture on Periodic Task Scheduling

The satellite ground station problem: only one signal at a time

In 1989, Robert Holte and colleagues at the University of Texas at Austin formalized a practical operational headache as a mathematical problem. Multiple satellites each transmit data at fixed intervals, but a ground station's antenna can receive from only one satellite at a time. For each satellite, the requirement is that it must be received at least once within every $a_{i}$ consecutive days. Can an infinite receiving schedule be constructed that satisfies this for every satellite? This question marked the birth of the pinwheel scheduling problem.

The structure of the problem is simple. There are $k$ jobs, and job $i$ must be executed at least once every $a_{i}$ days. Exactly one job can be executed per day. The question is whether such a schedule exists at all.

The quantity $D (A) = \sum_{i = 1}^{k} \frac{1}{a _{i}}$ , called the density, lies at the heart of this problem. It is the sum of each job's "execution frequency per day," and if this sum exceeds 1, scheduling is physically impossible—naturally, since only one job can be done per day, but the total required workload per day would exceed 1.

However, a density of 1 or less does not guarantee schedulability. The most famous counterexample is $(2, 3, m)$ for $m \geq 6$ . Its density is $\frac{1}{2} + \frac{1}{3} + \frac{1}{m} = \frac{5}{6} + \frac{1}{m}$ , which can be pushed arbitrarily close to 1 by increasing $m$, yet this set of periods is unschedulable no matter how large $m$ is chosen. The jobs with periods 2 and 3 interfere with each other in such a way that no permanent gap remains for the third job to be inserted.

From 0.5 to 0.75: a quarter-century of progress, only 0.083 gained

It was known early on that a sufficiently small density guarantees schedulability. In 1989, Holte and colleagues showed that density $\leq \frac{1}{2}$ suffices. From there began a race to push this threshold as high as possible.

Chan and Chin achieved density $\leq 0.7$ in 1992 using a double integer reduction technique, and in an Algorithmica paper the following year (1993) reported a result of $\leq \frac{2}{3}$ based on greedy scheduling. In 2002, Peter Fishburn and Jeffrey Lagarias of Bell Labs reached $\leq \frac{3}{4}$ . But progress beyond that point proved elusive.

Year	Researchers	Density Threshold	Method
1989	Holte, Mok, Rosier, Tulchinsky, Varvel	1/2 ≈ 0.500	Rounding periods to powers of 2
1992	Chan, Chin	0.700	Double integer reduction
1993	Chan, Chin	2/3 ≈ 0.667	Greedy scheduling
2002	Fishburn, Lagarias	3/4 = 0.750	Combinatorial analysis
2026	Kawamura	5/6 ≈ 0.833	Extension to real-valued periods + exhaustive computer search

In 1993, in a paper published in Algorithmica, Chan and Chin proposed a conjecture: that density $\leq \frac{5}{6}$ always guarantees schedulability, and that—given the existence of the $(2,3,m)$ counterexample—nothing higher could be hoped for. This "5/6 conjecture" remained the central open problem in real-time scheduling theory for more than 30 years.

There were partial results along the way: for cases with at most three distinct period values (Lin & Lin, 1997), for cases where the minimum period is 2 (Fishburn & Lagarias, 2002), for cases where each period value has five or more jobs (Baruah & Lin, 1998), and for cases with at most 12 jobs (Gąsieniec, Smith & Wild, 2022). The conjecture was confirmed in these special cases one by one, but no one had reached a general proof.

"Folding": the idea that collapses infinity into a finite set

When Akitoshi Kawamura presented an outline of his proof at STOC (the ACM Symposium on Theory of Computing) in Vancouver in June 2024, the core of his method turned out to be a surprisingly simple operation.

The overall structure of the proof has two stages. The first stage reduces the infinitely many "potentially unschedulable candidates" to a finite number of small instances. The second stage actually verifies that finite number of instances by computer.

The key to the first stage is an operation called "folding." For jobs whose period $a$ exceeds a threshold $θ$ , the following two operations are applied repeatedly:

If there is only one job with period $a$, shrink its period to the next-largest period value greater than $θ$ (if $a$ is the only period exceeding $θ$ , shrink it to $θ$ ).
If there are two or more jobs with period $a$, merge two of them into one, giving the merged job a period of $a/2$.

Both operations "preserve unschedulability"—that is, if the instance after the operation is schedulable, then the original instance was also schedulable. Repeating this operation transforms any instance into one where all periods are at most $θ$ . Kawamura chose $θ = 22$ . Folding with this value can be shown to increase the density by no more than $\frac{1}{22}$ .

Here a second refinement comes into play. Instances after folding can contain non-integer periods (for example, $\frac{55}{4} = 13.75$ ). Kawamura extended the problem itself to a version where periods may be any positive real number. A job with a non-integer period $r$ is redefined to require execution at least $⌊ t / r ⌋$ times within any span of $t$ days. This extension makes it possible to mathematically handle the intermediate instances that arise from the folding operation.

Replacing non-integer periods after folding with $⌈ b ⌉ - 1$ (the largest integer less than $b$) ultimately yields a finite set of instances, $C_{5/6}^{22}$ , in which all periods are integers less than 22. Proving that every instance in this set is schedulable proves the original conjecture.

A computer writes out 61,616 schedules

The second stage is an exhaustive computer search. The set $C_{5/6}^{22}$ is large. According to Kawamura's supplementary materials, the total number of instances satisfying the conditions reaches 25,592,971. Narrowing this down by minimality under set inclusion reduces it to 676,224, and further compression to those instances that actually require explicit schedules for verification brings the count down to 61,616.

Schedulability of each instance is determined using a "state graph" method. Each job's "remaining days until its next deadline" is represented as a state, and a cycle in the state transition graph indicates schedulability. Because the number of states grows in proportion to the product of the periods, it can balloon to exponential order, but Kawamura extended and implemented an efficiency technique from prior work (Gąsieniec, Smith & Wild, 2022) to handle this.

Thus, on August 7, 2026, the paper "Proof of the density threshold conjecture for pinwheel scheduling" appeared online in PNAS (Proceedings of the National Academy of Sciences) (DOI: 10.1073/pnas.2530214123). A conjecture that had stood unresolved for 33 years was finally settled.

The mirror-image covering problem: pinning down the optimal bound of 1.264...

Kawamura and Yusuke Kobayashi applied this method to a "mirrored" version of the problem as well: pinwheel covering.

Whereas the packing version imposes a lower-bound constraint—"job $i$ must be executed at least once within $a_{i}$ days"—the covering version imposes an upper-bound constraint: "agent $i$ may be assigned the task at most once within $a_{i}$ days." This corresponds to a situation where a single task that must be performed every day is shared among multiple agents.

Even in the covering version, density $D (A) = \sum \frac{1}{a _{i}} \geq 1$ is a necessary condition for schedulability, but it is not sufficient. $(2, 3, 5)$ satisfies density $\frac{1}{2} + \frac{1}{3} + \frac{1}{5} = \frac{31}{30} > 1$ , yet it can easily be shown that it cannot even cover 8 consecutive days without failure.

In 2020, Kawamura and Soejima showed that density $\geq 1.546$ guarantees schedulability, and conjectured that the true optimal value was $α^{*} = \sum_{i = 1}^{\infty} \frac{1}{2 ^{i - 1} + 1} = 1.264 \dots$ . This value is the limit toward which the density of the counterexample sequence $(2, 3, 5, 9, 17, \dots)$ —with periods $2^{i-1}+1$—converges as $k \to \infty$.

Kawamura and Kobayashi adapted the folding and real-valued-period techniques developed for the packing proof to the covering case and resolved this conjecture in the affirmative. They posted a preprint to arXiv (arXiv:2510.06533) in October 2025 and will present the result at ESA (the European Symposium on Algorithms) in August–September 2026. The covering case required verifying an even larger number of instances—25,242,331—and needed additional techniques such as parallel scheduling and state reduction via symmetry.

Ripple effects: a 4/3 approximation guarantee for bamboo trimming

The side effects of this work are not small. The "bamboo garden trimming problem" (BGT), closely related to pinwheel scheduling, involves $n$ bamboo stalks growing at different rates, where exactly one stalk can be cut per day, and the goal is to minimize the maximum height any stalk ever reaches. The performance of approximation algorithms for this problem is directly tied to the density threshold for pinwheel scheduling.

When the density threshold stood at $\frac{3}{4}$ , the best known approximation ratio for BGT was around $\frac{4}{3} + ε$ . With Kawamura's proof establishing the density threshold of $\frac{5}{6}$ , a fast algorithm with approximation ratio $\frac{4}{3}$ is now theoretically guaranteed. Notably, follow-up research inspired by this result has reported an improved approximation ratio of $\frac{9}{7} \approx 1.286$ (arXiv:2510.22060).

Metric	Previous (as of 2022)	This work (2026)
Density threshold (packing)	3/4 = 0.750 (Fishburn & Lagarias, 2002)	5/6 ≈ 0.833 (optimal value)
Density threshold (covering)	1.546 (Kawamura & Soejima, 2020)	α* = 1.264... (optimal value)
BGT approximation ratio (derived from this method)	4/3 + ε (based on density 3/4)	4/3 (based on density 5/6, fast online scheduler)
Instances verified (packing)	Up to 12 jobs (Gąsieniec et al., 2022)	61,616 (entire range of periods < 22)

Is a proof written by a computer still "mathematics"?

This proof is a "computer-assisted proof." The theoretical part guarantees why verifying a finite number of cases suffices, and the computer actually verifies that finite number. This has the same structure as the Four Color Theorem (1976) and the Kepler Conjecture (1998, with formal verification completed in 2017), though Kawamura himself has not ruled out the possibility of a simpler proof.

In Kyoto University's announcement, Kawamura said, "I haven't given up hope that a 'clean,' humanly readable proof might still be found in the future." At the same time, he noted, "Recent remarkable advances in computing technology, including AI, are bringing new possibilities and developments to mathematical research"—acknowledging that collaboration between computers and mathematics is becoming increasingly standard.

Indeed, the theoretical portion of this proof does have a beautiful, humanly readable structure: the invariance property of the folding operation, the extension to real-valued periods, the choice of threshold $θ = 22$ . These are all mathematical insights that do not depend on the computer. The computer's role was limited to the final stage of finite verification.

Questions remaining in the density "gaps"

During the course of the proof, computer experiments gave rise to a new conjecture. Instances that are unschedulable near density $\frac{5}{6}$ are overwhelmingly of the form $(2, 3, a_{3})$ or $(3, 4, 4, a_{4})$ . Kawamura proposed a conjecture (Conjecture 8) that for each minimum period $a_{1}$ , a density threshold of $1 - \frac{a _{1} - 1}{a _{1} ( a _{1} + 1 )}$ holds. For $a_{1} = 2$ , this gives $\frac{5}{6}$ ; for $a_{1} = 3$ , $\frac{11}{12}$ ; and for $a_{1} = 4$ , $\frac{17}{20}$ .

If this conjecture is correct, it would mean that instances with a larger minimum period remain schedulable even at higher densities, opening up further flexibility in implementation. However, proving this conjecture is thought to require a different kind of structural understanding than the technique used here.

Another open problem concerns the computational complexity of pinwheel scheduling. It has been known since 1989 that determining schedulability lies in PSPACE, but whether it belongs to NP or is NP-hard has remained undetermined for many years. A paper posted to arXiv in April 2026 (arXiv:2604.13974) claims NP-hardness, suggesting that this question, too, may soon be resolved.

An inequality that had been believed "probably true" for more than 30 years has now been settled—through the simple operation of folding and the explicit enumeration of 61,616 schedules. The next question is what new structure will come into view atop this now-established fact.