By combining environment exploration, hypothesis testing, and formal verification in Lean, AWM can rigorously prove that goals are unreachable—even beyond observed trajectories—enabling certified reasoning about unfamiliar worlds.
This paper presents Algebraic World Model (AWM), a system that explores unknown environments, builds executable Python hypotheses, and formalizes them as mathematical models in Lean 4 to prove what's possible and impossible. AWM discovered that certain game levels are unwinnable by constructing formal proofs, outperforming GPT and Claude on impossible-goal detection and game-solving tasks.