清华姚期智团队提出代数世界模型 AWM，让 AI 从探索走向形式化证明

清华大学姚期智、袁洋团队提出代数世界模型（AWM），把游戏中的对象、关系和规则抽象成代数世界，经探索、凝炼、证明三步形成可机器检查的 Lean 4 数学断言。