SHEAF

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

SHEAF框架将论文中的命题、定义及依赖关系组织成一张从目标定理逐层延伸到基础定理库的有向无环图，多个智能体围绕该图分工协作。