我个人已经跨越了一条界限，我对此感到有些敬畏。 这是我第一次完全自动化、由LLM生成并自动形式化的新数学定理的证明。 让我来设定问题：我们有三个旋转的圆，每个圆有六个位置，三者在总共六个点相交。 证明它们生成的运动群是完整的对称群 S_{12}。 这是我最初在Amanita Design的游戏《Machinarium》中注意到的一个可爱的难题。 这个任务并不是特别困难，但显然有两个证明： 1. 通过共轭类的暴力搜索来表示所有的置换（我在很多年前做过这个，但从未发表过）。 2. 一个LLM生成的证明（在这种情况下是大约三个月前由GPT-5-Pro生成的），实际上有两个证明，都是以一种聪明的方式使用了关于原始群的Jordan定理（或一个更直接的相关变体）。 直到今晚，我才发现缺少一个工具来自动形式化这个证明。 多亏了@HarmonicMath，我获得了他们出色的软件Aristotle的访问权限。总之，我所做的如下： A. 使用LLM自动生成证明（并多次运行以获得更好的版本）。 B. 将证明修剪到最基本的数学文本——定义、命题、引理、定理——由LLM提供证明。 C. 通过API在一夜之间运行Aristotle系统。今天早上，我收到了一个在Lean中完全形式化的版本（大约700行代码）。 代码可以编译，所以我现在有一个证书确认LLM生成的证明确实导致了正确的解决方案。此外，我得到了一个概念证明，比我自己的暴力搜索更好。我计划进一步推动到更广泛的代数问题类。 这是一个小项目，但对我个人来说，它标志着一个里程碑。我现在有工具，可以在我的协调下，真正帮助我发现、形式化和研究数学定理的证明。这并非易事。 问题： 1. 未来这将如何扩展？ 2. 成功完成此类任务需要多少培训？ 3. 我们应该如何对待这些证明的作者身份？ 4. 数学家的更深层角色是什么？

有人计划参加吗？ 这将会非常有趣！

我非常期待新架构的原因之一是，代数拓扑中的问题根本上需要超越简单符号操作的直觉。通常，呈现一个基于同胚/同伦的论证的视觉草图要比设计精确的公式并使其完全正式容易得多。 我希望世界模型、符号操作和物体动态的表示的结合是通向全新架构的一条道路。如果我们想解决超越单纯文本的困难数学问题，我们需要它们。 在这张图片中（基于arXiv: 2107.01664），你可以看到直观理解手铐悖论是多么容易，但用公式正式写出来又是多么困难。