combinatorics - 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.

Answer

Note that proving $$\sum_{k=1}^{\infty} \dfrac1{k^2} = \dfrac{\pi^2}6 \,\,\,\,\,\, (\spadesuit)$$ is equivalent to proving $$\sum_{k=0}^{\infty} \dfrac1{(2k+1)^2} = \dfrac{\pi^2}{8} \,\,\,\,\,\, (\clubsuit)$$ The hope for proving $(\clubsuit)$ instead of $(\spadesuit)$ is that squaring $\dfrac{\pi}4$ gives $\dfrac{\pi^2}{16}$ and adding this twice gives us $\dfrac{\pi^2}8$. We will in fact prove that $$\sum_{k=-\infty}^{\infty} \dfrac1{(2k+1)^2} = \left(\sum_{k=-\infty}^{\infty} \dfrac{(-1)^k}{(2k+1)} \right)^2$$
Since we know $$\sum_{k=0}^{\infty} \dfrac{(-1)^k}{(2k+1)} = \dfrac{\pi}4$$ and $$\sum_{k=0}^{N} \dfrac{(-1)^k}{(2k+1)} = \sum_{k=-(N+1)}^{-1} \dfrac{(-1)^k}{(2k+1)},$$
we have that $$\sum_{k=-\infty}^{\infty} \dfrac{(-1)^k}{(2k+1)} = \dfrac{\pi}2$$

Square the above to get
\begin{align}
\left(\sum_{k=-N-1}^{k=N} \dfrac{(-1)^k}{(2k+1)} \right)^2 & = \left(\sum_{k=-N-1}^{k=N} \dfrac{(-1)^k}{(2k+1)} \right) \left( \sum_{j=-N-1}^{j=N} \dfrac{(-1)^j}{(2j+1)} \right)\\
& = \sum_{k=-N-1}^{k=N} \sum_{j=-N-1}^{j=N} \dfrac{(-1)^{j+k}}{(2k+1)(2j+1)}\\
& = \sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{2(j-k)} \left(\dfrac1{(2k+1)} - \dfrac1{(2j+1)} \right) + \sum_{k=-N-1}^{k=N} \dfrac{(-1)^{2k}}{(2k+1)(2k+1)}
\end{align}
Hence,
$$\left(\sum_{k=-N-1}^{k=N} \dfrac{(-1)^k}{(2k+1)} \right)^2 - \sum_{k=-N-1}^{k=N} \dfrac{1}{(2k+1)(2k+1)} = \sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{2(j-k)} \left(\dfrac1{(2k+1)} - \dfrac1{(2j+1)} \right)$$
Let us now show that
$$\overbrace{\sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{2(j-k)} \left(\dfrac1{(2k+1)} - \dfrac1{(2j+1)} \right)}^{(\heartsuit)} \to 0 \text{ as } N \to \infty$$

We have
\begin{align}
(\heartsuit) & = \sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{2(j-k)} \dfrac1{(2k+1)} - \sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{2(j-k)} \dfrac1{(2j+1)}\\
& = \sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{2(j-k)} \dfrac1{(2k+1)} + \sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{2(k-j)} \dfrac1{(2j+1)}\\
& = 2 \times \left(\sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{2(j-k)} \dfrac1{(2k+1)} \right)\\
& = \sum_{\overset{j,k=-N-1}{j \neq k}}^{k=N} \dfrac{(-1)^{j+k}}{(j-k)} \dfrac1{(2k+1)} = \sum_{k=-N-1}^N \dfrac{(-1)^k}{(2k+1)} \underbrace{\left(\sum_{\overset{j=-N-1}{j \neq k}}^N \dfrac{(-1)^{j}}{(j-k)}\right)}_{(\diamondsuit_{k})}
\end{align}
Let us simplify $(\diamondsuit_{k})$ a bit. Assuming $k \neq -N-1$, we have
\begin{align}
\sum_{\overset{j=-N-1}{j \neq k}}^N \dfrac{(-1)^{j}}{(j-k)} & = \sum_{j=k+1}^N \dfrac{(-1)^{j}}{(j-k)} + \sum_{j=-N-1}^{k-1} \dfrac{(-1)^{j}}{(j-k)}\\

& = \left(\dfrac{(-1)^{k+1}}{1} + \dfrac{(-1)^{k+2}}{2} + \cdots + \dfrac{(-1)^{N}}{N-k}\right)\\
& + \left(\dfrac{(-1)^{k-1}}{(-1)} + \dfrac{(-1)^{k-2}}{(-2)} + \cdots + \dfrac{(-1)^{-N-1}}{-N-1-k}\right)\\
& = (-1)^{k+1} \sum_{j=N-\vert k \vert +1}^{N+\vert k \vert +1} \dfrac{(-1)^j}{j}
\end{align}
If $k = -N-1$, we have
$$\sum_{\overset{j=-N-1}{j \neq k}}^N \dfrac{(-1)^{j}}{(j-k)} = \sum_{j=-N}^N \dfrac{(-1)^{j}}{(j+N+1)} = (-1)^{N-1} \sum_{j=1}^{2N+1} \dfrac{(-1)^j}{j}$$
We now have
$$(\heartsuit) = \sum_{k=0}^N \dfrac{(-1)^k \diamondsuit_k + (-1)^{-k-1} \diamondsuit_{-k-1}}{2k+1} = \sum_{k=0}^N \dfrac{(-1)^k \left(\diamondsuit_k - \diamondsuit_{-k-1} \right)}{2k+1}$$
Now for $k \geq 0$
\begin{align}

\left(\diamondsuit_k - \diamondsuit_{-k-1} \right) & = (-1)^{k+1} \sum_{j=N-k +1}^{N+k +1} \dfrac{(-1)^j}{j} - (-1)^{-k} \sum_{j=N-(k+1) +1}^{N+(k+1) +1} \dfrac{(-1)^j}{j}\\
& = 2 \cdot (-1)^{k+1} \cdot \sum_{j=N-k+1}^{N+ k +1} \dfrac{(-1)^j}{j} + (-1)^{N+1} \left( \dfrac1{N+k+2} + \dfrac1{N-k}\right)
\end{align}
Hence,
$$\left \vert \diamondsuit_k - \diamondsuit_{-k-1} \right \vert = \mathcal{O} \left( \dfrac1N\right)$$
$$\left \vert (\heartsuit) \right \vert \leq \sum_{k=0}^N \dfrac1{2k+1} \mathcal{O}(1/N) = \mathcal{O}(\log(2N+1)/N) \to 0$$
Hence,
$$\left(\sum_{k=-N-1}^{k=N} \dfrac{(-1)^k}{(2k+1)} \right)^2 - \sum_{k=-N-1}^{k=N} \dfrac{1}{(2k+1)(2k+1)} \to 0$$
Hence,
$$\left(\sum_{k=-\infty}^{\infty} \dfrac{(-1)^k}{(2k+1)} \right)^2 = \sum_{k=-\infty}^{\infty} \dfrac{1}{(2k+1)(2k+1)} = 2 \sum_{k=0}^{\infty} \dfrac{1}{(2k+1)^2} = 2 \cdot \dfrac34 \cdot \zeta(2)$$

Hence,$$\boxed{\zeta(2) = \dfrac23 \cdot \dfrac{\pi^2}4 = \dfrac{\pi^2}6}$$