Topic: Lean theorem prover

Safe Cuts for Two-Rim Convex Bands: A geometric proof and Lean formalization

Let 𝐴 and 𝐵 be convex hulls of finite planar point sets, each with nonempty interior, and let ℎ > 0. We prove that the lateral surface of 𝐾 = conv((𝐵 × {0}) ∪ (𝐴 × {ℎ})) admits a static…