AI for Science:自我演化发现的黎明
本文基于曹原访谈,探讨数学、逻辑与物理世界的区别及AI在科学发现中的局限。AI擅长演绎推理,但跨越物理边界面临挑战。真正的科学智能需要从封闭学习空间转向开放式自我演化,通过实验反馈不断重构关系结构。
本文基于曹原访谈,探讨数学、逻辑与物理世界的区别及AI在科学发现中的局限。AI擅长演绎推理,但跨越物理边界面临挑战。真正的科学智能需要从封闭学习空间转向开放式自我演化,通过实验反馈不断重构关系结构。
文章回顾了人工智能与数学证明的深厚渊源,从1950年代的Logic Theorist到哥德尔不完备性定理,探讨了形式化数学的演进。重点介绍了现代AI数学的基础设施LEAN(包括其核心人物Leonardo de Moura、从v3到v4的演进及mathlib库),以及DeepMind、Harmonic、Axiom Math等科技巨头和初创公司在AI自动定理证明领域的布局。文章指出,AI正在通过神经网络与形式化验证的结合,重新回归逻辑推理的起点。