记者从北京大学北京国际数学研究中心了解到，该中心董彬教授课题组与合作者组建的 AI4Math 团队用自主构建的自动化 AI 框架解决了交换代数中一个开放问题 ——Anderson 猜想，并在 Lean 4 中完成了约 19000 行的形式化验证 … 这是国内首次以 AI 框架攻克交换代数开放问题并实现大规模形式化验证，开辟了数学与 AI 深度融合的更多可能 … 北京大学数学科学学院院长、中国科学院院士刘若川指出，此次探索不仅解决了具体数学问题，更验证了 AI 与数学融合的新研究范式。
暂无讨论，说说你的看法吧