33分钟完成一页证明：借助GitHub Copilot和Lean自动化工具的新尝试

最近，一位研究人员尝试使用现代自动化工具——特别是 Github Copilot 大型语言模型和依赖类型匹配战术 canonical——在 Lean 中半自动地形式化了“等式理论项目”（Equational Theories Project）合作者 Bruno Le Floch 提供的一页证明。整个过程仅用了33分钟，而研究者本人并没有对证明的整体思路有深入理解。这与他以往的形式化方法截然不同，但对于这样技术性强、概念性弱的论证来说，这一方法是可行的，因为重点在于准确捕捉细节而非把握大方向。 在这一过程中，这位研究者录制了自己的尝试视频，分享在了 YouTube 上（链接已省略）。此外，他还参与了 leanprover.zulipchat.com 上关于“等式理论项目”中的 E1689 方程替代证明方法的讨论（链接同样省略）。该讨论涉及了如何利用这些新技术提高数学证明的形式化效率，以及它们在这类特定任务上的适用性。 最终的形式化证明文件已发布在 GitHub 上（链接为 github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean）。虽然这个证明远未达到最优化的状态，但它成功地完成了任务，验证了这种方法的可行性。 这一实验不仅展现了大型语言模型和自动化工具在辅助数学证明领域的巨大潜力，也为形式化数学的未来发展打开了新的可能性。业内专家表示，随着技术的发展，这类工具将变得更加智能和可靠，有可能成为数学家不可或缺的助手。它们不仅能帮助解决繁琐的技术性问题，还可能会在某些领域发现新的定理或提供不同的证明思路。 Lean 是由微软研究院开发的开源交互式定理证明器，广泛应用于计算机科学和数学领域的研究中。它的强大之处在于能够支持高度抽象的数学概念，并通过严格的逻辑检查来确保证明的正确性。Github Copilot 则是由 GitHub 开发的人工智能编码助手，通过分析已有代码生成建议，从而帮助开发者更快地完成编程任务。两者的结合在本次实验中显示出了惊人的协同效应，未来或许会在形式化证明领域发挥更大的作用。