代数世界模型：从探索到证明

论文提出代数世界模型（AWM）框架，将陌生环境中的交互转化为可形式推理的显式数学模型：先探索环境并生成可执行Python假设，持续用观测检验和修正，再将假设组织为类型化对象与共享规则，经范畴论引导的变换化简，最后在Lean 4中形式化以证明可达性与不可能性。AWM在两个不可能通关的游戏关卡上构造了内核校验的Lean证明，证明目标不可达，且超出已探索轨迹。

AI推荐理由 提出代数世界模型（AWM），让AI在未知环境中探索、生成可执行Python假设并迭代修正，再经范畴论引导的结构化简，最终在Lean 4中形式化证明可达性与不可达性。新信息是能在已探索轨迹之外证明目标不可达，并在两个不可能通关的游戏关卡上构造内核校验的Lean证明；局限是实验规模小、仅限游戏环境，摘要未说明通用性。