This is a Lean-verified variation of the OpenAI proof for pi.