大湾区大学许地生团队借助国产多模态大模型与 Harness 系统，经人机协同攻克困扰数学界 30 年的三维 Ghys 猜想，北大团队用 Lean 完成 55 万行代码形式化验证，首次实现中国大模型破解世界级数学难题。