AI的下一个风口？听前DeepSeek成员辛华剑解读数学推理 | Deep Talk

4 月 30 日，DeepSeek在 AI 开源社区 Hugging Face 上，发布名为 DeepSeek-Prover-V2-671B 的新模 型。 这是一款专注于形式化数学推理的开源大型语言模型。 数学推理长期以来被视为AI的"终极挑战"之一。形式化数学不仅是AI的"智力试金石"，更是打开高价值商业场 景的钥匙。DeepSeek-Prover系列模型通过结合LLM的泛化能力与形式化工具（如Lean），首次实现了从自 然语言描述到机器可验证证明的大规模端到端转化。这一突破不仅可能将数学研究效率提升数倍，更将为AI在 金融建模、芯片验证、密码学等依赖数学严谨性的领域打开新可能性。 5月9日，DeepSeek前成员辛华剑，也将参加剑桥大学中国人工智能协会、锦秋基金、清华大学学生通用人工 智能协会、清华大学学生创业协会合作的"大模型开发者与AI基金合伙人的跨洋对谈活动"。他将进行《大语言 模型时代的形式化数学革命》的主题分享。 辛华剑现在是爱丁堡大学人工智能博士生、字节跳动研究实习生，专注于大语言模型在数学定理证明中的创新 应用。他在DeepSeek实习期间主导开发了专注于数学证明DeepSeek-Prove ...