This is a "visual proof" of the Archimedean limiting regular polygons. You could implement the recursion and it would progressively approach $\pi$. The proof lies in the "squeezing" argument. $\pi$ is transcendental (no solution to this recurrence in a closed algebraic expression). Whatever implementation of recursion with approach $\pi$ that is reassuring but not proof.
This is a slight modification. The $\pi$ approximation from half the circumference of the inscribed and circumscribed polygons. f
is one way to implement recursion. The "geometric" method just calculates length of polygon side (euclidean distance of points):
f[n_, {a_, b_}] :=
Nest[
{2 #1 #2/(#1 + #2), #2 Sqrt[2 #1/(#1 + #2)]} & @@ # &,
{a, b}, n]
g[n_] := Module[{pi = Table[{Cos[j], Sin[j]}, {j, 0, 2 Pi, 2 Pi/n}],
pe = Table[Sec[Pi/n] {Cos[j], Sin[j]}, {j, 0, 2 Pi, 2 Pi/n}]},
{Graphics[{Circle[{0, 0}, 1], FaceForm[White], EdgeForm[Red],
Polygon[pi], FaceForm[None], EdgeForm[Blue], Polygon[pe],
Line[{{0, 0}, #}] & /@ pe[[{1, 2}]],
Text["\!\(\*SubscriptBox[\(β\), \(n\)]\)",
0.9 Mean[pi[[{1, 2}]]]],
Text["\!\(\*SubscriptBox[\(α\), \(n\)]\)",
1.1 Mean[pe[[{1, 2}]]]]
}], (Norm[#1 - #2]/2) & @@@ {pe[[{1, 2}]], pi[[{1, 2}]]}}]
dem[n_, r_] := Module[{s = g /@ PowerRange[n, n 2^(r - 1), 2], i},
i = s[[1, 2]];
MapIndexed[
Flatten[{#2[[1]] - 1, #1[[1]], N[#1[[2]]],
N[n 2^(#2[[1]] - 1) #1[[2]]], N[f[#2[[1]] - 1, 2 n i]/2]}] &,
s]]
Visualizing:
TableForm[dem[6, 4],
TableHeadings -> {None, {"n", "Polygons",
"\!\(\*SubscriptBox[\(α\), \(n\)]\)",
"\!\(\*SubscriptBox[\(β\), \(n\)]\)",
"\!\(\*SubscriptBox[\(Pi\), \(geometric\)]\)\n \
\!\(\*SubscriptBox[\(a\), \(n\)]\)",
"\n \!\(\*SubscriptBox[\(b\), \(n\)]\)",
"\!\(\*SubscriptBox[\(Pi\), \(recursion\)]\)\n \
\!\(\*SubscriptBox[\(a\), \(n\)]\)",
"\n \!\(\*SubscriptBox[\(b\), \(n\)]\)"}}]

Just for illustrative purposes (would have to very careful for arbitrary precision):
st[n_] :=
Module[{a = RealDigits[n, 10, 20][[1]],
pi = RealDigits[N[Pi, 20]][[1]], lg, pos, a1},
pos = FirstPosition[a - pi, _?(# != 0 &)];
a1 = StringJoin@(ToString /@ a);
Row[{Style[StringTake[a1, 1], Red, Bold], ".",
Style[StringTake[a1, 2 ;; pos[[1]]], Red, Bold],
StringTake[a1, pos[[1]] + 1 ;;]}]
]
fn[n_, {a_, b_}] :=
Nest[
N[{2 #1 #2/(#1 + #2), #2 Sqrt[2 #1/(#1 + #2)]}, 40] & @@ # &,
{a, b}, n]
res = fn[#, {4 Sqrt[3], 6}]/2 & /@ Range[0, 20];
So,
TableForm[
Map[st, res, {2}],
TableHeadings ->
{Range[0, 20],
{"\!\(\*SubscriptBox[\(a\), \(n\)]\)",
"\!\(\*SubscriptBox[\(b\), \(n\)]\)"}}
]
