看到近期AI在数学领域攻城略地，感叹当年的【神经符号计算】真是误入歧途了。数学是纯粹的符号计算，基于纯神经网络的LLM在数学领域的表现已经超过人类，还有什么问题是必须借助符号方法解决而不能仅用神经网络解决的呢？不过仔细一想，也不能这么说，现在的AI数学定理证明，Lean语言的验证才能确保证明过程的正确性，仅仅依靠AI生成的证明过程，是不能保证正确性的。这本身就是完美的【神经符号计算】。当然，Lean语言的验证只是为证明的正确性提供了形式化的验证，最终AI在数学上取得超过人类数学家的成功，还是由AI模型的能力突飞猛进取得的。从这个意义上讲，AI在这个【神经符号计算】的突破中扮演了更重要的角色。不管怎么样，【神经符号计算】这个研究课题，应该可以告一段落了。