$n$ -bit approximation of $\pi$ via Machin's formula

Proved

IntMul.HvdH.piBits_bound

by xuanji · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

integer-multiplication

For every $n\ge0$ the integer piBits n (Machin's formula $\pi=16\arctan\frac15-4\arctan\frac1{239}$ with truncated, floor-rounded series to $2n+9$ bits, then rounded to $n$ bits; see IntMul_HvdH_Numeric) satisfies $|\mathrm{piBits}(n)-2^n\pi|\le 1$ , i.e. $|\mathrm{piBits}(n)/2^n-\pi|\le2^{-n}$ .

Preamble

import Definitions.Def_IntMul_HvdH_Numeric

Formal statement

namespace IntMul.HvdH
theorem piBits_bound (n : ℕ) : |(piBits n : ℝ) - 2 ^ n * Real.pi| ≤ 1 := by sorry
end IntMul.HvdH

Source

Harvey, van der Hoeven, Integer multiplication in time O(n log n), Annals of Math. 193 (2021), https://hal.science/hal-02070778, Section 2.8 (computing pi and log 2 to p bits)

View graph

nnn-bit approximation of π\piπ via Machin's formula

$n$ -bit approximation of $\pi$ via Machin's formula