Formalizing a proof in Lean using Github Copilot only

In this video, I test how Github Copilot performs in formalizing some basic "epsilon delta" type proofs in analysis. The final Lean file: https://github.com/teorth/estimate_to... For comparison, here is a somewhat similar demonstration by Alex Kontorovich on similar problems from 2022, in Lean 3 (rather than the current Lean 4) and before the advent of large language models:    • Prof. Kontorovich, Informal Lecture on Mat...   . A more recent (Lean 4) version of the talk, with a demonstration on how to get started in Lean, can be found at    • How Mathematicians can Get Started with Lean