沈策｜AI-Assisted Mathematical Research（11 月 24 日）

北京时间　11 月 24 日（周二）13:30–16:55

Zoom 会议号　435 529 7909　｜　密码　BIMSA　一键加入 Zoom (opens in a new tab)

沈策的系列课讨论如何把大语言模型、数学软件和 Lean 4 用于数学研究，包括调用计算工具检验例子、把长证明拆成引理，以及用 Lean 核查模型给出的证明。本条目对应 11 月 24 日的课次，也可以到 BIMSA A3-1a-205 现场参加。主办方课表及教学大纲 (opens in a new tab)