数学家与上海人工智能实验室Intern-S2合作证明1995年Ghys猜想的三维情形，并用Lean完成验证（媒体报道）

已核实（事实）

据Pandaily报道，数学家与上海人工智能实验室的模型Intern-S2进行多轮对话，构建出Étienne Ghys于1995年提出的猜想中余维数（codimension）为1的情形的证明。随后，北京大学团队用定理证明语言Lean将该证明形式化并完成验证。

意义（解读）

这并不是AI独自给出答案的案例，而是与人类多轮对话构建证明、并完成Lean形式化验证的案例。在近期围绕AI数学成果可信度的争议中，它提供了一种可验证协作方式的范例。

来源

• 媒体 Mathematicians Use Shanghai AI Lab's Intern-S2 to Prove 3D Ghys Conjecture, Verified in Lean Pandaily