Irrationality of $\pi$ another proof

Proposition. Let $\alpha\in\mathbb{R}$. If there is a sequence of integers $a_n,b_n$ such that $0<|b_n\alpha-a_n|\longrightarrow 0^+$ as $n\longrightarrow \infty$, then $\alpha$ is irrational.

How to prove that $\pi$ is irrational using this proposition?

I know several proof of the irrationality of π with complex analysis, but I think in this way is very difficult.

For example to prove the irrationality of $e$ consider

$$0<n!e-n!\left(1+\frac{1}{2!}+\frac{1}{3!}+\cdots +\frac{1}{n!}\right)\le\frac{1}{n}\longrightarrow0^+$$

Any hint would be appreciated.

The classical proof that $\pi$ is irrational is due to Lambert and rests on his continued fraction expansion expression for $\tan x$. I include below a proof that a continued fraction expansion is irrational and the application to the irrationality of $\pi$. I copied these from notes that I made for myself some time ago so I hope they are comprehensible, I can also post a proof of the Lambert expansion if you wish. The only references I know are old (very old) there is a two volume algebra book by Chrystal, and an old french calculus book by Bertrand which have information on this material.

In the continued fraction, $$\cfrac{b_1}{a_1 - \cfrac{b_2}{a_2 - \cfrac{b_3}{a_3 - \cfrac{b_4}{a_4 -\cdots}}}} $$ assume that where $1+b_n \leq a_n$ for all $n$, and that we have $1+b_n < a_n$ infinitely often. Then the fraction is irrational. $a_n, b_n$ integers.

Proof Assume that the fraction is rational, say $$\frac{\lambda_1}{\lambda_0}=\cfrac{b_1}{a_1 - \cfrac{b_2}{a_2 - \cfrac{b_3}{a_3 - \cfrac{b_4}{a_4 -\cdots}}}} $$ where $\lambda_1$ and $\lambda_0$ are positive integers, now since the fraction converges to a number less than one, $\lambda_1 < \lambda_0$ If we set $$\rho_1=\cfrac{b_2}{a_2 - \cfrac{b_3}{a_3 - \cfrac{b_4}{a_4 -\cdots}}} $$ then we have $$\frac{\lambda_1}{\lambda_0}=\frac{b_1}{a_1 -\rho_1}$$ so$$\rho_1=\frac{a_1 \lambda_1 - b_1 \lambda_0}{\lambda_1} < 1$$ So $\rho_1=\frac{\lambda_2}{\lambda_1}$ where $\lambda_2 < \lambda_1$.

Continuing in this way we obtain a strictly decreasing sequence of positive integers, $\lambda_0 > \lambda_1 > \cdots$, a contradiction.

[Lambert] $$\tan x=\cfrac{x}{1- \cfrac{x^2}{3-\cfrac{x^2}{5-\cfrac{x^2}{7-\cdots}}}}$$

This expression leads to the following fundamental result.

Theorem [Lambert] $\pi$ is irrational.

Proof Assume that $\pi$ is rational, then $\frac{\pi}{4}$ is also rational. Let $$\frac{\pi}{4}=\frac{a}{b},$$ and substitute $x=\frac{\pi}{4}$ into Lambert's continued fraction for $\tan x$.

We get \begin{equation*} \begin{split} 1=&\cfrac{\frac{a}{b}}{1- \cfrac{\frac{a^2}{b^2 }}{3-\cfrac{\frac{a^2 }{b^2}}{5-\cfrac{\frac{a^2}{b^2}}{7-\cdots}}}} \\ &=\cfrac{a}{b- \cfrac{a^2}{3b-\cfrac{a^2}{5b-\cfrac{a^2}{7b-\cdots}}}} \\ \end{split} \end{equation*} Now since eventually $nb > a^2 +1$ we have that this expression is irrational, and this is absurd since it is equal to $1$. Therefore $\pi$ is irrational.

If we assume $ \pi = \lim_{n \to \infty} [\sum_{i=1}^n \sqrt{n^2-(i-1)^2}]{4 \over n^2}$ (which can be obtained by applying a riemann sum over a half circle function $y = \sqrt{R^2-x^2}$, on the interval $[0,r]$), we have a structure like the one you used for $e$, I guess. It isn't an integer, but can be a hint.

From the irrationality and uniformity of $\pi$ it follows, that such a sequence exists. Numerically you could easily construct it (look for increasingly long sequences of zeros in eg. the binary representation and use the string before that point as $a_n$ with a $b_n$ of the form $2^m$). Unfortunately that does not help you in proving the irrationality of $\pi$.

From the definition $|b_n \alpha - a_n|\rightarrow 0$ it is obvious, that $\frac{a_n}{b_n}$ is an approximation to $\alpha$. In fact, let $e_n=\left|\alpha - \frac{a_n}{b_n}\right|$ denote the error of the $n$-th approximation, then (for infinitely many $n$)

$$ \begin{align} \left|b_n\alpha - a_n\right| &< \left|b_{n-1}\alpha - a_{n-1}\right| \\ \Rightarrow e_n &= \left|\alpha - \frac{a_n}{b_n}\right| \\ &<\frac{b_{n-1}}{b_n} \left|\alpha - \frac{a_{n-1}}{b_{n-1}}\right| \\ &=\frac{b_{n-1}}{b_n} e_{n-1} \end{align} $$

which implies superlinear convergence of $\frac{a_n}{b_n}\rightarrow\pi$.

Unfortunately I am not aware of a sequence that converges superlinearly to $\pi$. The best I know gives 16 bits per iterations - linearly. Deconstructing such a sequence into $a$ and $b$ we would have $b_n=2^{16}b_{n-1}$ and $e_n = 2^{-16}e_{n-1}$ which clearly would not satisfy the above inequality.

Still, as I only know a small fraction of all the sequences converging to $\pi$ that exist, looking for one that satisfies this necessary condition and checking whether you can deconstruct it into $a_n$ and $b_n$ might be your best bet.