E9 和DeepSeek-Prover作者辛华剑聊「形式化数学」：数学的工业化，Agentic AI，Benchmark

本期海外独角兽邀请了 DeepSeek-Prover 系列核心作者辛华剑，探讨数学与 AGI 之间的关系。辛华剑介绍了形式化数学的概念，它与传统数学的不同，以及为何选择 Lean 作为训练语言。讨论了数学作为研究对象对其他领域的益处，Prover 的含义，DeepSeek-Prover 系列的进展，以及 LM 在数学领域扮演的角色。还探讨了合成数据在数学研究中的应用，A-Bench benchmark 的设计思路，以及未来 AI 和 LLM 可能突破的瓶颈，如 reward agent 的训练和 online learning 的实现。最后，对 AGI 的实现时间线和技术发展方向进行了展望。