【北大AI把数学猜想的活儿干了，还自己给自己验算】刚看到一条挺炸的消息：北大董彬团队的AI4Math，用自研的双智能体框架，搞定了交换代数里一个十几年没人动的开放问题——Anderson猜想。这不是让AI算个题或者猜个结果，而是从自然语言推理、到生成反例、再到在Lean 4里写出19000行形式化验证，全程自己跑通。而且这个过程中，AI还发现自己一开始的逻辑有漏洞，自己改了方案；碰到数学库里没收录的概念，自己找了等价替代路径。效率据说是人类Lean专家的10倍以上。说白了，这套系统已经不只是“算得快”，而是能主动检索、推理、纠错、验证，形成一个闭环。团队还专门做了个语义检索引擎Matlas，能从上千万条数学陈述里精准捞到看似无关但能用的定理。这不是“AI辅助数学”，这是AI在独立推数学。当然，目前还在特定领域和框架下，但方向已经很明显了：以后数学家可能真得跟AI搭档干活了。不是取代，是加速。 http://t.cn/AXMPDSmZ