pi

Description

The cosine function has exactly one zero in the interval $[0, 2]$. The number $\pi$ is twice this zero. So $\cos(\pi/2) = 0$, and $$\pi \approx 3.14159265.$$

Remarks

A zero exists by the intermediate value theorem, since $\cos 0 = 1$ and $\cos 2 < 0$. It is unique because $\cos$ is strictly decreasing on $[0, 2]$, by its derivative $-\sin$. With this definition, $\pi$ is the ratio of the circumference of a circle to its diameter, and the area of the unit disc. Mathlib defines Real.pi in the same way, as twice the zero of $\cos$ in $[1, 2]$. William Jones first used the letter $\pi$ for this ratio, in 1706. Around 250 BC, Archimedes approximated $\pi$ with regular polygons.

Explanations

L1 human

The number $\pi$ is the length of half of the unit circle. In analysis, we find it through the first positive zero of cosine, which is $\pi/2$.