#### 内容简介 本文介绍了数学家陶哲轩对人工智能（AI）、Lean等形式化证明工具，以及未来数学家的角色变化的看法。他认为AI目前主要作为辅助工具，帮助数学家检验证明、探索新想法，但距离独立创作数学尚有距离。他看好形式化工具能提升数学验证和协作效率。陶哲轩强调，数学家的创造力、直觉和逻辑并不会被机器轻易取代，未来数学创造仍需人机协作推动。 #### 社区观点 社区认为AI和形式化证明工具正逐步改变数学研究的方式，Lean等工具减少了低级错误，增强了团队配合。目前AI还不能完全替代数学家的原创性和直觉，但协助性作用已非常显著。未来，人与AI的合作可能成为数学创新的主要途径，数学家会把更多精力放在创意思考和方向引领上，而具体验证和细节则更多交给AI和工具来实现。 #### 内容导读 想知道AI和未来工具会如何改变数学家和数学本身吗？本文带你走近陶哲轩的独特视角，了解顶级学者如何判断AI、Lean软件对专业数学领域的深刻影响，以及人机协作在创新中的前景和挑战。