# Polynomial-time scheduling on three identical machines

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A Polynomial-Time Algorithm for Three-Machine Unit-Job Scheduling](../../preprints/A-polynomial-time-algorithm-for-three-machine-unit-job-scheduling-September-24-2026/paper.pdf)

## Scope

The formalization gives a deterministic polynomial-time algorithm for scheduling nonempty collections of unit-length jobs with arbitrary acyclic precedence constraints on three identical parallel machines. It constructs a schedule of minimum makespan and decides exactly whether a valid specified deadline can be met. The algorithm is one fixed finite machine, and its running time is bounded by a polynomial in the binary input length.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Optimal three-machine unit-job scheduling | [ThreeMachine.lean](../ComparatorChallenges/ThreeMachine.lean) |