Scheduling unit jobs with precedence constraints on three machines
From OpenAI Aftermath
Scheduling unit jobs with precedence constraints on three machines is the problem P3 | prec, pj = 1 | Cmax: given unit-length jobs with acyclic precedence constraints, find a schedule on three identical machines of minimum makespan. Whether it can be solved in polynomial time is listed as problem OPEN8 in Garey and Johnson's book and has been a central open question in scheduling theory. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a deterministic polynomial-time algorithm. The collection includes a Lean formalization of this statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- The two-processor case was treated by Fujii, Kasami and Ninomiya, and Coffman and Graham gave an optimal list-scheduling algorithm; with the number of machines part of the input the problem is NP-complete, by Ullman. The fixed three-machine decision problem appears as OPEN8 in Appendix A13 of Garey and Johnson.
- Garey, Johnson, Tarjan and Yannakakis gave a linear-time algorithm on three processors for opposing forests, Dolev and Warmuth obtained an algorithm polynomial for fixed height of the precedence graph and fixed number of processors, and Nederlof, Swennenhuis and Węgrzycki gave an exact algorithm with running time 2O(√n log n) for three machines.
The original result
- Claim. Theorem 1.1 of A polynomial-time algorithm for three-machine unit-job scheduling states that for an explicitly listed directed acyclic graph of precedence constraints on n ≥ 1 unit-length jobs on three identical machines there is a uniform deterministic algorithm that constructs a feasible schedule of minimum makespan and, given a deadline 1 ≤ T ≤ n, decides feasibility exactly, both in O((L + 2)150020) steps on a deterministic multitape Turing machine, where L is the binary input length. The manuscript states that the exponent is very large and that no practical running-time claim is made.
- Method, as described: a dynamic program over sets of jobs described by Boolean formulas of bounded size, built from rank thresholds and membership tests; its completeness rests on a structure theorem stating that every feasible schedule has a recursive decomposition into a center and separator walks whose node sets have descriptions of bounded size.
- Sources. The manuscript A polynomial-time algorithm for three-machine unit-job scheduling at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization gives a deterministic polynomial-time algorithm for scheduling nonempty collections of unit-length jobs with arbitrary acyclic precedence constraints on three identical machines, constructing a schedule of minimum makespan and deciding whether a specified deadline can be met, as one fixed finite machine with running time polynomial in the binary input length. The Comparator statement is
ThreeMachine.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full", with no review note, stating that the polynomial exponent 150020 is explicit and that the machine is fixed before the instance. Among the definitions to check it lists the hand-written multi-tape Turing machine model used instead of Mathlib's polynomial-time computability notion. It records Comparator passes for the challenge, with and without a sandbox. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-08 | drbh/scheduling-proof-exploration (GitHub) | Remark (exploratory adaptation) | Copies the collection's Lean scheduling development and changes it so that each time slot allows four jobs, describing the work as an educational exploration of adapting the proof from three machines to four, made with the help of AI models. The README states that the author is not a mathematician, that the explanations and the reading of the formal statement may be wrong, and asks specialists to review the specification and the changes. | GitHub repository; the README gives build instructions but reports no build result. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38040214623 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the ThreeMachine solution, in 499 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list ThreeMachine, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. The reviewer states that it read every proof in the manuscript's sections and checked by hand the soundness and completeness of the dynamic program, the exchange arguments in the separator walks, the edge labels and update identities, and the description-size bounds. | Part of an audit of the collection's manuscripts that the audit describes as complete. The review is published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
