It is User:wonghang.

Proof of Leibniz formula

Proof of Wallis product

Basel problem

Machin's formula

${\displaystyle {\frac {\pi }{4}}=4\tan ^{-1}{\frac {1}{5}}-\tan ^{-1}{\frac {1}{239}}}$

Recall the formulas:

${\displaystyle \tan(x+y)={\frac {\tan x+\tan y}{1-\tan x\tan y}}}$

${\displaystyle \tan(x-y)={\frac {\tan x-\tan y}{1+\tan x\tan y}}}$

${\displaystyle \tan(2x)={\frac {2\tan x}{1-\tan ^{2}x}}}$

Let

${\displaystyle \tan \alpha ={\frac {1}{5}}}$

We can obtain tan(2α) = 5/12 and tan(4α) = 120/119 by using the above formula. Therefore,

${\displaystyle \tan(4\tan ^{-1}{\frac {1}{5}})={\frac {120}{119}}}$

Consider,

${\displaystyle \tan(4\tan ^{-1}{\frac {1}{5}}-\tan ^{-1}{\frac {1}{239}})={\frac {{\frac {120}{119}}-{\frac {1}{239}}}{1+{\frac {120}{119}}{\frac {1}{239}}}}={\frac {120\cdot 239-119}{119\cdot 239+120}}={\frac {120(120+119)-119}{119(120+119)+120}}={\frac {120^{2}+119^{2}}{120^{2}+119^{2}}}=1}$

${\displaystyle 4\tan ^{-1}{\frac {1}{5}}-\tan ^{-1}{\frac {1}{239}}={\frac {\pi }{4}}}$

Q.E.D.