Formalizing a proof in Lean using Github copilot and canonical

In this experiment, I took a statement in universal algebra that a collaborator of mine (Bruno Le Floch) on the Equational Theories Project had written a one-page human proof of, and set the task of formalizing the proof in a very low-level, "line by line" fashion, with heavy reliance on both the large language model-powered code completion tool "Github Copilot" and the dependent type matching tactic "canonical". The proof was formalized in about 33 minutes. Further discussion: https://leanprover.zulipchat.com/#nar... The final proof: https://github.com/teorth/estimate_to... A followup video:    • Formalizing a proof in Lean using Claude a...   General links: Lean: https://lean-lang.org/ A user friendly place to get acquainted with Lean is the Natural Number Game: https://adam.math.hhu.de/ Github Copilot: https://github.com/features/copilot Canonical: https://github.com/chasenorman/Canoni... Note that Canonical does not currently ship in the default installation of Lean, and must be installed separately.