Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Buffon's Needle Problem


view this post on Zulip Email Gateway (Aug 22 2022 at 15:36):

From: Tobias Nipkow <nipkow@in.tum.de>
Buffon's Needle Problem
Manuel Eberl

In the 18th century, Georges-Louis Leclerc, Comte de Buffon posed and later
solved the following problem, which is often called the first problem ever
solved in geometric probability: Given a floor divided into vertical strips of
the same width, what is the probability that a needle thrown onto the floor
randomly will cross two strips? This entry formally defines the problem in the
case where the needle's position is chosen uniformly at random in a single strip
around the origin (which is equivalent to larger arrangements due to symmetry).
It then provides proofs of the simple solution in the case where the needle's
length is no greater than the width of the strips and the more complicated
solution in the opposite case.

https://www.isa-afp.org/entries/Buffons_Needle.shtml

This is another one off the list of 100 Theorems.
smime.p7s


Last updated: Mar 29 2024 at 04:18 UTC