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