近日，OpenAI等AI巨头强势杀入数学界，接连挑战千禧年猜想与ETH假设等硬核难题。AI之所以“死磕”数学，关键在于Lean等数学形式化证明系统。它能将证明转化为严谨代码，为AI提供可靠的验证反馈，不仅助力大模型实现自我进化（RSI），还能有效消除AI幻觉。不过，Lean也存在死板、无法判断命题价值等局限，且难以套用于复杂的现实世界。尽管AI在解决“怎么做”上不断突破，但决定“为什么做”的最终解释权，依然牢牢掌握在人类手中。无需过度焦虑，AI终究是人类的工具。