形式化证明与大模型：共创可验证的AI数学未来｜量子位直播

5月，多个重要进展引发关注：DeepSeek Prover V2发布、陶哲轩的AI数学直播以及谷歌推出的AlphaEvolve。大模型在解数学题方面的表现已成为衡量AI“智能天花板”的关键指标，吸引了众多团队投入研究。

为更好评估AI的数学推理能力，近期发布的FormalMATH基准测试受到广泛关注。那么，当前AI自动定理证明的表现如何？主要技术路径有哪些？其对大模型的应用又将产生什么影响？

5月29日晚20:00，量子位联合2077AI开源基金会举办直播活动，邀请DeepSeek Prover、FormalMath、Kinima等项目的多位专家探讨大语言模型在形式化证明领域的前沿探索。

直播嘉宾
- 辛华剑，爱丁堡大学博士生，DeepSeek Prover项目第一作者
- 刘威扬，香港中文大学博士生导师，资深学者
- 付杰，上海人工智能实验室研究员，人工智能领域专家
- 郁昼亮，香港中文大学博士生，FormalMath项目第一作者
- 王海明，月之暗面（Moonshot AI）技术负责人，Kinima项目技术领衔人
- 刘征瀛，月之暗面（Moonshot AI）技术负责人，资深技术专家
- 李祎哲，浙江大学博士生，数学领域青年研究者
- 刘明皓，资深算法工程师，2077AI核心发起人、贡献者

直播议程
详见附图

本周四晚20:00，让我们一起探讨AI数学的未来！