Precedence-constrained Scheduling of Unit Jobs is Polynomial for Every Fixed Number of Machines

SummaryIn the scheduling problem P_m | prec, p_j = 1 | C_max, n jobs of unit length, subject to precedence constraints given by a directed acyclic graph, are to be scheduled on m identical machines so as to minimize the makespan. The two-machine case was solved in 1969–1972. The three-machine case was listed as an open problem by Garey and Johnson in 1979, and the complexity has been open for every constant number of machines. In 2026 OpenAI released a polynomial-time algorithm for three machines together with a Lean formalization. This work builds on that development and extends it to every number of machines. Main results Every fixed number of machines (Theorem 1.1). For every m ≥ 1, a multitape Turing machine solves the optimization and deadline versions of the problem in C_m (|x|+2)^{d_m} steps, where d_m = 70m² + 247m + 10. For three machines the exponent is 1376, compared with 150020 in OpenAI’s statement. The exponent is quadratic rather than cubic in m because the formula leaves describing the sets handled by the dynamic program are counted per list entry rather than uniformly. A single algorithm for all m (Theorem 1.2). One algorithm that receives m as part of its input runs within f(m)·(n+|E|+1)^{56m²+199m+7} steps in a RAM cost model with declared operation prices. The problem parameterized by the number of machines is therefore in XP. Since it is W[2]-hard (Bodlaender–Fellows), it is not fixed-parameter tractable unless FPT = W[2]. Lower bound (Theorem 1.4). A direct reduction from k-Clique produces instances with m = k + 3 machines. Under the k-Clique hypothesis, for every fixed m ≥ 8 no algorithm runs in time O(n^{ω(m−3)/9 − δ}), where ω is the matrix-multiplication exponent. So the optimal exponent lies between a linear and a quadratic function of m. Verification Theorem 1.1 is proved in Lean 4 with Mathlib, using only the standard axioms (propext, Classical.choice, Quot.sound) and no sorry. The development is re-checked by Lean’s kernel module by module (87 of 87 modules), by a full from-scratch kernel replay, and by nanoda, an independent kernel implementation (26,329 declarations). For Theorem 1.2, correctness and the cost bound are checked in Lean relative to the declared cost model. The lower bound is proved on paper. Its reduction was checked on 419 instances with two independent SAT solvers and an independent re-implementation.