A small start on formally proving graceful paths and caterpillars in Lean.
https://prideout.net/blog/graceful-lean/