形式化证明与大模型：共创可验证的AI数学未来

就在 5 月，前有发布，后有，还有谷歌最新发布的。

大模型 " 解数学题 " 的能力已经是衡量 AI「智能天花板」的一种方式，正吸引着无数团队争相挑战。

为了更好地评估 AI 完成数学推理的能力，近期发布的也备受关注。

现在，AI 完成自动定理证明的表现与挑战究竟如何？主流的技术路径是什么？AI 完成形式化证明的能力，又将对大模型应用带来怎样的影响？

为了回答这些问题，5 月 29 日 20:00，我们与 2077AI 开源基金会共同邀请到了来自DeepSeek Prover、FormalMath、Kinima等项目团队的成员，一同来讨论大语言模型形式化证明前沿探索。

点击下方按钮，一键预约直播  

直播嘉宾

辛华剑，爱丁堡大学博士生，DeepSeek Prover 项目第一作者

刘威扬，香港中文大学博士生导师，资深学者

付杰，上海人工智能实验室研究员，人工智能领域专家

郁昼亮，香港中文大学博士生，FormalMath 项目第一作者

王海明，月之暗面（Moonshot AI）技术负责人，Kinima 项目技术领衔人

刘征瀛，月之暗面（Moonshot AI）技术负责人，资深技术专家

李祎哲，浙江大学博士生，数学领域青年研究者

刘明皓，资深算法工程师，2077AI 核心发起人、贡献者

直播议程

本周四晚 20:00，一起来聊聊AI 数学吧～

一键三连「点赞」「转发」「小心心」

欢迎在评论区留下你的想法！

—  完  —

 量子位 AI 主题策划正在征集中！欢迎参与专题365 行 AI 落地方案，一千零一个 AI 应用，或与我们分享你在寻找的 AI 产品，或发现的AI 新动向。

也欢迎你加入量子位每日 AI 交流群，一起来畅聊 AI 吧～

一键关注 点亮星标

科技前沿进展每日见