<s>[INST] Can the Basel problem be solved by Leibniz today? It is well known that Leibniz derived the series
$$\begin{align}
\frac{\pi}{4}&=\sum_{i=0}^\infty \frac{(-1)^i}{2i+1},\tag{1}
\end{align}$$
but apparently he did not prove that
$$\begin{align}
\frac{\pi^2}{6}&=\sum_{i=1}^\infty \frac{1}{i^2}.\tag{2}
\end{align}$$
Euler did, in 1741 (unfortunately, after the demise of Leibniz). Note that this was also before the time of Fourier.
My question: do we now have the tools to prove (2) using solely (1) as the definition of $\pi$? Any positive/negative results would be much appreciated. Thanks!
Clarification: I am not looking for a full-fledged rigorous proof of (1)$\Rightarrow$(2). An estimate that (2) should hold, given (1), would qualify as an answer.
 [/INST] One of the best way without leibnizSince $\int_0^1 \frac{dx}{1+x^2}=\frac{\pi}{4}$, we have
$$\frac{\pi^2}{16}=\int_0^1\int_0^1\frac{dydx}{(1+x^2)(1+y^2)}\overset{t=xy}{=}\int_0^1\int_0^x\frac{dtdx}{x(1+x^2)(1+t^2/x^2)}$$
$$=\frac12\int_0^1\int_t^1\frac{dxdt}{x(1+x^2)(1+t^2/x^2)}\overset{x^2\to x}{=}\frac12\int_0^1\left(\int_{t^2}^1\frac{dx}{(1+x)(x+t^2)}\right)dt$$
$$=-\frac12\int_0^1\frac{\ln\left(\frac{4t^2}{(1+t^2)^2}\right)}{1-t^2}dt\overset{t=\frac{1-x}{1+x}}{=}-\frac12\int_0^1\frac{\ln\left(\frac{1-x^2}{1+x^2}\right)}{x}dx$$
$$\overset{x^2\to x}{=}-\frac14\int_0^1\frac{\ln\left(\frac{1-x}{1+x}\right)}{x}dx=-\frac14\int_0^1\frac{\ln\left(\frac{(1-x)^2}{1-x^2}\right)}{x}dx$$
$$=-\frac12\int_0^1\frac{\ln(1-x)}{x}dx+\frac14\underbrace{\int_0^1\frac{\ln(1-x^2)}{x}dx}_{x^2\to x}$$
$$=-\frac38\int_0^1\frac{\ln(1-x)}{x}dx\Longrightarrow \int_0^1\frac{-\ln(1-x)}{x}dx=\frac{\pi^2}{6}$$

Remark:
This solution can be considered a proof that $\zeta(2)=\frac{\pi^2}{6}$ as we have $\int_0^1\frac{-\ln(1-x)}{x}dx=\text{Li}_2(x)|_0^1=\text{Li}_2(1)=\zeta(2)$
</s>