The two projects of github:schildep are "3d mesh intersection" and "multipolygon intersection". I can try "Voronoi diagram generation" as a starter.
Inspired by two projects of github:schildep I start to explore what can be expressed in Lean and make coding agents implement and prove the implementation at the same time.