Kyoto University Proves 33-Year-Old "5/6 Conjecture," Setting a Theoretical Limit for Periodic Task Scheduling

The "only one satellite at a time" problem faced by ground stations

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. A ground station's antenna can receive from only one satellite at a time. Can an infinite receiving schedule be constructed that satisfies, for every satellite, the requirement of "receiving at least once within any $a_{i}$ consecutive days"? This question marked the beginning of the pinwheel scheduling problem.

The structure of the problem is simple. There are $k$ tasks, and task $i$ must be executed at least once every $a_{i}$ days. Exactly one task can be executed per day. The goal is to determine whether a valid schedule exists.

The quantity $D (A) = \sum_{i = 1}^{k} \frac{1}{a _{i}}$ , called the density, holds the key to this problem. It is the sum of each task's "execution frequency per day," and if this exceeds 1, scheduling is physically impossible—naturally so, since only one task can be completed per day, yet 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 made arbitrarily close to 1 by increasing $m$—yet this combination remains unschedulable no matter what value of $m$ is chosen. A task with a 2-day period and one with a 3-day period interfere with each other, leaving no permanent gap in which to fit the third task.

From 0.5 to 0.75: a quarter-century advance of just 0.083 in the density threshold

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

Chan and Chin achieved density $\leq 0.7$ in 1992 via double integer reduction, and in an Algorithmica paper the following year 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 stalled from there.

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 their 1993 Algorithmica paper, Chan and Chin posed a conjecture: that density $\leq \frac{5}{6}$ always guarantees schedulability, and that—given the $(2,3,m)$ counterexample—no higher bound could be hoped for. This "5/6 conjecture" would remain the central open problem in real-time scheduling theory for more than 30 years.

Partial results did accumulate: for cases with three or fewer distinct period values (Lin & Lin, 1997); for cases where the minimum period is 2 (Fishburn & Lagarias, 2002); for cases where each period value is shared by five or more tasks (Baruah & Lin, 1998); and for cases with 12 or fewer tasks (Gąsieniec, Smith & Wild, 2022). The conjecture was confirmed correct in special cases one after another, but no one reached a general proof.

"Folding": a shift in thinking that compresses 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 proof has two stages. In the first stage, the infinitely many "potentially unschedulable candidates" are reduced to a finite number of small instances. In the second stage, that finite set of instances is actually verified by computer.

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

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

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

Here a second innovation 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 task with a non-integer period $r$ is redefined to require "at least $⌊ t / r ⌋$ executions within any $t$ days." This extension makes it possible to mathematically handle the intermediate instances produced by folding.

Replacing each non-integer period 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. If every instance in this set can be shown to be schedulable, the original conjecture is proven.

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 material, the total number of qualifying instances reaches 25,592,971. Narrowing this down by minimality under inclusion relations reduces it to 676,224, and the number of instances actually requiring an explicit schedule for verification is compressed further to 61,616.

Schedulability of each instance is determined by a "state graph method." The "remaining days until the next deadline" for each task is represented as a state, and if a cycle exists in the state transition graph, the instance is schedulable. Because the number of states grows in proportion to the product of the periods, it balloons exponentially—but Kawamura extended and implemented the efficiency techniques 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" was published online in PNAS (Proceedings of the National Academy of Sciences of the United States of America; DOI: 10.1073/pnas.2530214123). A conjecture unresolved for 33 years had finally been settled.

The optimal bound of 1.264... also confirmed for the "inverted" covering variant

Kawamura and Yusuke Kobayashi applied this method to a "mirror-image" problem as well: pinwheel covering.

Whereas packing imposes a lower-bound constraint—"task $i$ must be executed at least once within $a_{i}$ days"—covering 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.

For covering as well, density $D (A) = \sum \frac{1}{a _{i}} \geq 1$ is a necessary condition for schedulability, but 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 maintain coverage for 8 days.

In 2020, Kawamura and Soejima showed that density $\geq 1.546$ guarantees schedulability and conjectured that the optimal value is $α^{\*} = \sum_{i = 1}^{\infty} \frac{1}{2 ^{i - 1} + 1} = 1.264 \dots$ . This value is the limit to which the density of the counterexample sequence $(2, 3, 5, 9, 17, \dots)$ —that is, the sequence 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, resolving this conjecture affirmatively. They posted a preprint on arXiv in October 2025 (arXiv:2510.06533) and will present the result at ESA (the European Symposium on Algorithms) in August–September 2026. For covering, the number of instances requiring verification was even larger, at 25,242,331, necessitating additional techniques such as parallel scheduling and symmetry-based state reduction.

A ripple effect: a guaranteed 4/3 approximation ratio for bamboo trimming

The side effects are not trivial either. The "bamboo garden trimming problem" (BGT), closely related to pinwheel scheduling, involves cutting exactly one of $n$ bamboo stalks—each growing at a different rate—per day, with the goal of minimizing the height of the tallest stalk. The performance of approximation algorithms for this problem is directly tied to the density threshold of pinwheel scheduling.

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

Metric	Previous (as of 2022)	This work (2026)
Packing density threshold	3/4 = 0.750 (Fishburn & Lagarias, 2002)	5/6 ≈ 0.833 (optimal value)
Covering density threshold	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)
Number of verified instances (packing)	Range with ≤12 tasks (Gąsieniec et al., 2022)	61,616 (full range with periods < 22)

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

This proof is a "computer-assisted proof." The theoretical part guarantees "why checking a finite number of cases suffices," while a computer actually verifies that finite set. 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 more concise proof.

In Kyoto University's announcement, Kawamura stated, "I have not given up hope that a 'beautiful,' humanly readable proof may still be found in the future." At the same time, he remarked, "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 the norm.

Indeed, the theoretical portion of this proof contains a beautiful, humanly readable structure: the preservation property of the folding operation, the extension to real-valued periods, and the choice of threshold $θ = 22$ . These are mathematical insights independent of any computer. The computer's role was limited to the final finite verification step.

A question remaining in the density "gap"

During the course of the proof, computer experiments gave rise to a new conjecture. Among density- $\frac{5}{6}$ -adjacent instances that are unschedulable, those of type $(2, 3, a_{3})$ and type $(3, 4, 4, a_{4})$ account for the vast majority. Kawamura proposed a conjecture (Conjecture 8) stating that, for each minimum period $a_{1}$ , a density threshold of $1 - \frac{a _{1} - 1}{a _{1} ( a _{1} + 1 )}$ holds. This gives $\frac{5}{6}$ for $a_{1} = 2$ , $\frac{11}{12}$ for $a_{1} = 3$ , and $\frac{17}{20}$ for $a_{1} = 4$ .

If this conjecture is true, instances with a larger minimum period would be schedulable even at higher densities, further expanding the freedom available in implementation. However, proving this conjecture is thought to require a structural understanding different from the method used here.

Another open problem concerns the computational complexity of the pinwheel scheduling problem. That the schedulability decision problem lies in PSPACE has been known since 1989, but whether it belongs to NP or is NP-hard remained unresolved for years. A paper submitted to arXiv in April 2026 (arXiv:2604.13974) claims NP-hardness, suggesting a resolution in this direction may also be near.

An inequality believed, for more than 30 years, to be "probably true" has now been settled through the simple operation of folding and the explicit writing-out of 61,616 schedules. The next question is what structures will come into view atop this now-established fact.