Another Proof That 22/7 Exceeds pi

Proof

Notice that

$$ \begin{array}{ccl} \pi & = & \int_{0}^{2-\sqrt{3}} \frac{12}{1+x^2} dx \\ & < & \int_{0}^{2-\sqrt{3}} 12(1-x^2+x^4) dx \\ & = & \left. 12(x - \frac{x^3}{3} + \frac{x^5}{5}) \right|_{0}^{2-\sqrt{3}} \\ & = & \frac{3944 - 2268\sqrt{3}}{5}. \end{array} $$

It’s easy to verify that

$$ \frac{3944 - 2268\sqrt{3}}{5} < \frac{22}{7}. $$

Therefore, the proof is completed.

The story

From somewhere (now I cannot remember the exact place, probably YouTube), I found a math problem: Prove that

$$ \pi < \sqrt{2} + \sqrt{3}. $$

I could not do it, and I asked AI (Gemini and ChatGPT). AI provided a proof, in which the main steps are:

1. $\pi < 22/7$
2. $22/7 < \sqrt{2} + \sqrt{3}$

Step 2 is trivial, but Step 1 is not. So, I asked AI how to prove

$$ \pi < 22/7 $$

AI led me to this Wikipedia article Proof that 22/7 exceeds π. Dalzell’s proof is really cool!

The above story happened a couple of months ago. Today, I asked Gemini again to prove

$$ \pi < \sqrt{2} + \sqrt{3}. $$

Without surprise, Gemini gave me the same proof having the above two steps. Then, I asked Gemini to construct a new proof that is similar to Dalzell’s proof of $\pi < 22/7$. Gemini struggled, but its answers helped me find the following identity, which I think is a gem:

$$ \pi = \int_{0}^{\tan(\pi/k)} \frac{k}{1+x^2} dx,\ \hbox{for}\ k>2. $$

With that insight and notice

$$ \tan\left(\frac{\pi}{12}\right) = 2 - \sqrt{3} $$

plus

$$ \frac{1}{1+x^2} \le 1 - x^2 + x^4, $$

we can now fully understand the proof given at the beginning of this post.

Remarks

1. I’m reporting another (nice) proof of $\pi < 22/7$, but I’m not sure if the proof is original or it had been published somewhere and AI just “borrowed” ideas from there.
2. To calculate

$$ \begin{array}{l} & \left. \left[12(x - \frac{x^3}{3} + \frac{x^5}{5})\right] \right|_{0}^{2-\sqrt{3}} \\ = & \frac{3944 - 2268\sqrt{3}}{5} \end{array} $$

I used symbolic operations, and R code is included below

library(reticulate)

py_require("sympy")

sympy <- import("sympy")

exact_eval <- function(f, value) {
  x <- sympy$symbols("x")
  
  # Convert R expression to a SymPy expression
  f_str <- paste(deparse(f), collapse = "")
  f_sym <- sympy$sympify(f_str)
  
  val_sym <- sympy$sympify(value)
  
  sympy$simplify(
    f_sym$subs(x, val_sym)
  )
}

exact_eval(quote(12*(x - x^3/3 + x^5/5)), "2 - sqrt(3)")

## 3944/5 - 2268*sqrt(3)/5