Michail Karatarakis｜Formalizing Mathematics in Lean with AI（第 2 讲）

北京时间　11 月 12 日（周四）22:00 至次日 00:00

线上参加　请在 11 月 8 日 前通过CRM 课程页 (opens in a new tab)报名。主办方会在开课前把线上链接发给已注册者。

这是四次实作课中的第 2 讲。系列课从阅读 Lean 命题入手，讨论如何用 AI 把数学结果形式化，并核对机器验证的命题是否准确表达了原定理。主讲人鼓励参加者带上自己研究中的一个结果。