Kenny Peng, Jon Kleinberg, and Nikhil Garg; Working paper, 2026.
This paper’s Lean formalization is maintained in a separate repository.
Code size: 39,335 lines in 157 tracked Lean files at revision 4cac3256. The website includes this code in its total; Mathlib and other dependency code are excluded.