Comment by jdb1729

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