刘若川

北京大学董彬教授、刘若川院士团队利用自主开发的SHEAF框架对三维Ghys猜想证明进行了形式化验证，确认其严格正确性，通过Lean检验。

北京大学董彬教授、刘若川院士团队完成本次论文全部四个主定理的形式化验证，整个过程仅约5天，峰值并发达100个智能体，产出约55万行Lean代码。