### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Probability theory
- Mathematics/Geometry

### Session Buffons_Needle

- Buffons_Needle

## Cite

×

Buffons_Needle-AFP

    @article{Buffons_Needle-AFP,
      author  = {Manuel Eberl},
      title   = {Buffon's Needle Problem},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Buffons_Needle.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jun 6, 2017 : Isabelle2016-1