Meta AI 的 François Fleuret：AI 数学将让人类数学彻底边缘化

Meta AI 研究科学家 François Fleuret 认为，AI 数学之于人类数学将如同 CPU 每秒十亿次算术运算之于笔算，要求 AI 数学成果对人类可解释只是「可理解性税」，并不现实。他主张把重点转向机器可验证的形式化基础设施：推动 lean proofs 标准化与开放性，并强化、多样化 Lean 验证器等工具链。