Mathematician Uses Github Copilot and Lean to Rapidly Formalize Complex Proof in 33 Minutes

I recently embarked on an exercise to use modern automated tools, specifically a combination of Github Copilot, a large language model, and the dependent type matching tactic "canonical," to semi-automatically formalize a one-page proof provided by my collaborator, Bruno Le Floch, as part of the Equational Theories Project. Using these tools, I managed to complete the formalization in just 33 minutes, without a deep understanding of the proof's overall structure. This approach contrasts significantly with my usual method of formalizing results, which typically requires a high-level conception of the proof. However, it proved effective for this type of technical, detailed argument, where the primary focus is on getting the specifics right rather than grasping the broader picture. To document this process, I recorded my attempt and uploaded it to YouTube. You can view the video here. For further insights and discussions surrounding this project, you can visit the Lean Prover community forum here. The final proof, though not yet optimized, is available on GitHub here. This exercise highlights the potential of automated tools in streamlining the formalization process, especially for proofs that are more about precise details than conceptual frameworks. While traditional methods emphasize a deep understanding of the proof, these tools enable a more efficient, detail-oriented approach. They can significantly reduce the time and effort required, making the process more accessible and feasible for a broader range of mathematicians and computer scientists. However, it's important to note that such tools are still in their early stages, and the final product could benefit from further refinement and optimization. Overall, the experience suggests that these tools have the potential to revolutionize how we handle formal proofs in the future.