Mathematicians work with Shanghai AI Lab's Intern-S2 to prove 3D case of 1995 Ghys conjecture, verified in Lean (report)

Verified (fact)

According to Pandaily, mathematicians produced a proof of the codimension-one case of a conjecture posed by Étienne Ghys in 1995 through multiple rounds of dialogue with Shanghai AI Lab's model Intern-S2. A Peking University team then formalized and verified the proof in the theorem-proving language Lean.

Why it matters (interpretation)

This is not a case of AI producing an answer on its own. Humans built the proof through repeated dialogue with the model and then completed formal verification in Lean. Amid recent disputes over the reliability of AI-generated math results, it offers an example of a verifiable collaboration method.

Sources

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