形式化验证

稍早之前的4月，北京大学北京国际数学研究中心的AI4Math团队的董彬和刘若川、肖梁等人宣布：他们构建的自动化AI框架解决了交换代数中的安德森（Anderson）猜想，并在定理证明器Lean4中完成了形式化验证。