Buffon's Needle in Lean 4 A formalization of Buffon's Needle in Lean 4. The file Rewrite.lean contains the theorems buffons_short and buffons_long, which are the easy and hard case respectively of the problem.