It is rather embarrassing that, as a professional mathematician, that I didn't know how to prove the irrationality of $\pi$. The most common proof of this fact is this argument which PlanetMath cites to Hardy and Wright, but which I've seen also referred to in Bourbaki. I will discuss a slightly different proof here. The version that I read is from Zhou and Markov, though the idea is due originally to Lambert in 1761.

The following proof is an expanded version of the one given by Zhou and Markov.

First we observe that implicit in the theorem is that $\tan(r)$ is defined for any rational $r$. On the other hand, we know that the tangent is not defined at $k\pi / 2$ where $k$ is an integer. But we note that if we can prove the theorem for $r \in \mathbb{Q} \setminus \{ k\pi / 2 \}$ where $k \in \mathbb{Z}$ (in other words, for rational numbers *that are not the forbidden values*), we have sufficient knowledge to show that $\pi/4$ is irrational. With this we can bootstrap our initial assumption: since $\pi/4$ is irrational, the set of all rational numbers not equal to $k\pi / 2$ is precisely the set of all rational numbers not equal to 0.

With this observation, we set out to prove the "weakened" statement assuming $r \in \mathbb{Q} \setminus \{ k\pi / 2 \}$. We prove by contradiction. Assume that $r = a/b$ is a fixed rational number with $a,b$ nonzero integers, and assume that $\tan(r) = p/q$ where $p,q$ are also integers.

Consider the following sequence of functions: \[ f_n(x) = \frac{(r^2 - x^2)^n}{2^n n!} \] and the associated integrals: \[ I_n = \int_0^r f_n(x) \cos(x) dx \]

First we observe that \begin{equation} |b^n I_n| \leq \int_0^r \frac{(a^2 - b^2x^2)^n}{(2b)^n n!} |\cos(x)| dx \leq \int_0^r \frac{a^{2n}}{(2b)^n n!} dx = \frac{2a^{2n+1}}{(2b)^{n+1} n!} \end{equation} which implies that $\lim_{n\to\infty} b^nI_n = 0$. This is because of the strong factorial decay in the denominator of the definition of $f_n(x)$. Using the convention that $0! = 1$, we see that $f_0(x) = 1$ and $f_1(x) = (r^2 - x^2) / 2$. A computation then shows that \[ \begin{aligned} I_0 &= \int_0^r \cos(x)dx = \sin(r) \newline I_1 &= \int_0^r \frac{r^2-x^2}{2} \cos(x) dx = \left.\frac{r^2-x^2}{2}\sin(x)\right]^r_0 + \int_0^r x\sin(x) dx \newline &= 0 - \left.x\cos(x)\right]^r_0 + \int_0^r\cos(x) dx = \sin(r) - r\cos(r) \end{aligned} \] where in the computation for $I_1$ we integrated by parts twice.

Secondly we can observe a functional recursion for the numbers $I_n$. Assume $n \geq 2$, then \[ \begin{gathered} f'_n(x) = \frac{(r^2 - x^2)^{n-1}}{2^n (n-1)!} \cdot (- 2x) = - x f_{n-1}(x) \newline f''_n(x) = (-x f_{n-1}(x))' = - f_{n-1}(x) + x^2 f_{n-2}(x) \end{gathered} \] Observing that \[ x^2f_{n-2}(x) = - (r^2 - x^2)f_{n-2}(x) + r^2 f_{n-2}(x) = - 2(n-1) f_{n-1}(x) + r^2f_{n-2}(x) \] we arrive at the equation \[ f''_n(x) = r^2f_{n-2}(x) - (2n-1) f_{n-1}(x) . \] We plug this expression into $I_n$ and integrate by parts \begin{equation} I_n = \int_0^r f_n \cos dx = f_n\sin ]_0^r - \int_0^r f'_n\sin dx = f'_n\cos ]_0^r - \int_0^r f''_n\cos dx. \end{equation} Noting that $f_n(r) = 0$ for $n > 0$, we have also that $f'_n(0) = f'_n(r) = 0$ for $n > 1$. Therefore if $n \geq 2$, we have that \begin{equation} I_n = (2n-1)I_{n-1} - r^2 I_{n-2} \end{equation} Comparing with the expressions already derived for $I_0,I_1$, the recursion relation implies immediately that $I_n = u_n \sin(r) + v_n \cos(r)$ where $u_n,v_n$ are polynomials of $r$ with integer coefficients, and degree at most $n$. (We can prove this by induction: the recursion relation implies that if the statement is true for $I_{n-1},I_{n-2}$, then it is true for $I_n$. The starting hypothesis is easily checked for $I_0,I_1$.)

A further implication of the recursion relation is that if two consecutive terms $I_{n}, I_{n-1}$ are both zero, the entire sequence must all vanish identically. So our knowledge that $I_0, I_1$ are not both vanishing implies that infinitely many of the terms $I_n$ are non-zero.

Now, for our fixed $r \neq k\pi / 2$, we know that $\cos(r) \neq 0$, so we can divide the expression \[ I_n / \cos(r) = u_n \tan(r) + v_n .\] By our initial hypothesis, if we multiply through by the integer $q$, we have \[ q I_n / \cos(r) = p u_n + q v_n.\] Lastly, using that $u_n,v_n$ are polynomials of $r$ of degree at most $n$, we see that if we multiply through by $b^n$, the expressions $b^nu_n,b^nv_n$ now are polynomials of $a,b$ of degree at most $n$ with integer coefficients, and so are integers themselves. In other words, we have shown that for any $n$, \begin{equation} \frac{q b^n I_n}{\cos(r)} \in \mathbb{Z}. \end{equation} On the other hand, observe that $q / \cos(r)$ is just a fixed constant. Since we know that $b^nI_n$ tends to zero as $n$ grows to infinity, we can choose some large $N$ such that for any $n > N$, we have $|b^n I_n| \leq |\cos(r) / (2q)|$. Furthermore, since the sequence $I_n$ has infinitely many non-vanishing terms, we can choose some number $m > N$ such that \begin{equation} 0 < \left|\frac{q b^m I_m}{\cos(r)}\right| < 1 \end{equation} which is clearly absurd as we've also shown that the term in the middle must be an integer! Therefore our initial assumption must be false, and the theorem is proved.