{"id":"palomar/PALOMAR-2026-10-18-000021","url":"https://github.com/JD-Jones-ASES/graham-lpt-lean/tree/c8ed035b407cc554faf4b68df0cf3edc70058977","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000021-v1.json","repo":"https://github.com/JD-Jones-ASES/graham-lpt-lean","tags":["cs.DS","msc:90B35","msc:68W25","msc:68Q25","scheduling","approximation-bounds","lean"],"score":0,"title":"Graham's bounds for list scheduling and LPT on identical machines: 2 − 1/m, 4/3 − 1/(3m) and their tight instances","trust":"high","domain":"cs.DS","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"cs.DS","summary":"A Lean 4 development of Graham's two bounds for scheduling independent jobs on identical machines to minimize the makespan (R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Tech. J. 45 (1966) 1563-1581; Bounds on multiprocessing timing anomalies, SIAM J. Appl. Math. 17 (1969) 416-429; both restated with their examples in his survey Bounds on multiprocessing anomalies and related packing algorithms, AFIPS Spring Joint Computer Conference (1972) 205-217). n jobs of nonnegative real lengths p : Fin n -> R are run without interruption on m >= 1 identical machines; an…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"Bounds on multiprocessing timing anomalies","identifier":"doi:10.1137/0117039","relationship":"formalizes"},{"title":"Bounds for certain multiprocessing anomalies","identifier":"doi:10.1002/j.1538-7305.1966.tb01709.x","relationship":"formalizes"},{"title":"Elements of Scheduling","identifier":"arXiv:2001.06005","relationship":"formalizes"},{"title":"The Longest Processing Time rule for identical parallel machines revisited","identifier":"doi:10.1007/s10951-018-0597-6","relationship":"formalizes"},{"title":"Graham's example is the only tight one for P || Cmax","identifier":"https://annales-math.elte.hu/annales47-2004/Annales_Universitatis_Scientiarum_Budapestinensis_de_Rolando_Eotvos_nominatae_Sectio_Mathematica_2004_TOMUS_XLVII.pdf","relationship":"formalizes"}]}