摘要:本讲座将深度解析大语言模型在数学领域从“竞赛解题”到“科研协作者”的演进历程。我们将回顾 NuminaMath、Qwen、OpenAI o1、DeepSeek R1 及 Gemini DeepThink 在非形式化推理上的范式革命,并结合 DeepSeek-Prover 与 Seed-Prover 等前沿工作,探讨如何利用 Lean 等形式化语言(Formal Math) 构建自动验证体系,从根本上解决大模型的幻觉问题。最后,讲座将展望 AGI 视角下数学科研的新未来,分析 AI 如何重塑数学家的工作流,并为学生在 AI 时代如何平衡数学逻辑与编程技能提供实质性建议。
主讲人介绍:Project Numina的创始人,前Cardiologs的创始人兼CTO。Project Numina是一个开源的致力于促进AI在数学领域发展的组织,其数学大模型赢得了AIMO委员会设立的第一届AIMO progress prize,后续也开源出了NuminaMath 数据集和Kimina prover 等一系列的工作。
主讲人介绍:Project Numina的创始人,前Cardiologs的创始人兼CTO。Project Numina是一个开源的致力于促进AI在数学领域发展的组织,其数学大模型赢得了AIMO委员会设立的第一届AIMO progress prize,后续也开源出了NuminaMath 数据集和Kimina prover 等一系列的工作。
