four_mul_arctan_inv_5_sub_arctan_inv_239

English

4 arctan(1/5) − arctan(1/239) = π/4.

Русский

4 arctan(1/5) − arctan(1/239) = π/4.

LaTeX

$$$4 \\\\arctan\\\\left(\\\\frac{1}{5}\\\\right) - \\\\arctan\\\\left(\\\\frac{1}{239}\\\\right) = \\\\frac{\\\\pi}{4}.$$$

Lean4

/-- **John Machin's 1706 formula**, which he used to compute π to 100 decimal places. -/
theorem four_mul_arctan_inv_5_sub_arctan_inv_239 : 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4 := by
  rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one, sub_eq_iff_eq_add,
      arctan_add] <;>
    norm_num

Похожие утверждения