🤖 AI 辅助证明 Erdős 数论难题，形式化验证确保逻辑无误 Harmonic 公司开发的 AI 系统 Aristotle 近期在解决 Erdős 第 728 号数学难题中取得了突破性进展。该系统利用大语言模型技术将非正式的英文证明翻译为 Lean 形式化编程语言，并由 Lean 的微内核进行逻辑校验。这种方法的核心在于将 AI 的搜索能力与形式化验证的严谨性相结合：一旦证明通过 Lean 检查，即可确保其逻辑绝对正确，从而消除了生成式 AI 常见的"幻觉"问题。 在解决过程中，Aristotle 展现了"准自主"的特性。虽然最初的尝试需要人类专家（如数学家 Terence Tao）提供反馈以明确问题定义，但 AI 随后能够独立识别逻辑漏洞并完成证明修复。Terence Tao 将此能力定义为"通用聪明（General Cleverness）"，强调 AI 在快速重写、重构复杂论证以及利用现有方法解决难题方面的巨大潜力。 目前，Aristotle 已向 Lean 的数学库 Mathlib 提交了多项贡献。尽管该技术在拓扑学等缺乏形式化定义的领域仍受限，但在代数和数论等基础完备的领域，它已能显著加速科研迭代。这一进展标志着数学研究范式的转变，即从单纯的人类推导转向"人类设定目标、AI 搜索路径、机器严苛验证"的协作模式。 (HackerNews)