Latent Dynamics · 2026-10-30
Algebraic World Model: From Exploration to Proofs
Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao
AI-assisted summary based on the paper. Consult the linked source for methods and limitations. Benchmark numbers appear after editor verification.
TL;DR
The authors introduce the Algebraic World Model (AWM), a framework that explores an unknown environment to build executable Python hypotheses, restructures them into a compact algebraic model via category-theory-guided transformations, and formalizes the result in Lean 4 to prove reachability and impossibility. They report kernel-checked impossibility proofs on two impossible ARC-AGI-3 levels and full clearing of 25 public games with score 99.9.
Why it matters
AWM targets rigorous reasoning about unknown worlds by learning an explicit, inspectable model and then producing kernel-checked Lean proofs that apply beyond explored trajectories. The paper emphasizes model-relative impossibility (excluding all legal winning sequences under the learned model) and connects formal models to replay of winning trajectories and generalization to unseen transitions.
Method
- Explore & Prototype: actively probe the environment and maintain a concept book of executable Python hypotheses with checkers and optional predictors; revise concepts by rechecking against expanded transition data.
- Structure & Simplify: extract typed object types and rewrite concepts into rules, then apply four category-theory-guided transformations using projective/inductive limits, with Lean-checked auxiliary universal properties and preservation of previously detected rejections.
- Formalize & Prove: complete the model in Lean 4 and construct closed, kernel-checked proofs for reachability and impossibility, enabling theorems over all legal action sequences under the learned model.
Limitation
They describe post-hoc certificate audits as not additional agent-produced proofs, and note that fixed-opening scope is distinct from a four-opening ground-truth search; they also state that proof does not guarantee the underlying model correctly describes the game.
Abstract (from arXiv)
AI has made remarkable progress in mathematics, solving challenging problems with machine-checkable proofs in Lean, yet typically relying on predefined mathematical definitions and formal specifications. This raises a natural question: can it reason rigorously about an unknown world? We introduce the Algebraic World Model (AWM), a framework that turns interaction with unfamiliar environments into explicit mathematical models supporting formal reasoning. AWM explores the environment and develops executable Python hypotheses, continually testing and revising them against observations. It then structures these hypotheses into typed objects and shared rules, simplifies their structure through category-theory-guided transformations, and formalizes the resulting model in Lean 4 to prove reachability and impossibility. AWM can formally prove that a goal is unreachable, even beyond explored trajectories. On two impossible game levels, it constructs closed, kernel-checked Lean proofs excluding every legal winning sequence in all six runs, while Claude Opus 5.5 and GPT-6 Astra, equipped with coding tools, produce none in twelve baseline runs. Four of AWM's six initial bounds are correct, compared with one for Opus 5.5 and none for GPT-6 Astra; given only feedback that a cheaper win exists, AWM revises its rules and constructs new proofs, reaching six of six correct bounds. Moreover, AWM produces interpretable mathematical models whose rules can be inspected and tested step by step. Across all 25 public ARC-AGI-3 games, these models enable Lean to replay the winning trajectories of all 183 levels and generalize beyond observed play, predicting unseen transitions and detecting changes in game mechanics. With Claude Opus 5, AWM clears all levels with a score of 99.9, while its certified winning trajectories use only 43% of the human baseline's actions.
Related papers
Publication record
Bibliographic evidence describes where and when a record appeared. It does not validate scientific claims.
First public release: 2026-10-29 · Indexed by Pub-AI: 2026-10-30 UTC
Algebraic World Model: From Exploration to Proofs
Preprint posted: 2026-10-29 · Original record ↗
- arxiv
- 2610.40503
Explicit source versions (1)
- v1 · 2026-10-29
- Preprint available
Source date: 2026-10-29 · First detected: 2026-10-30 UTC · Historical baseline
Source evidence (2)
- Official evidence ↗ · RSS guid=oai:arXiv.org:2610.40503v1; arxiv:announce_type=new; item pubDate (official metadata)
- Official evidence ↗ · atom:published (official metadata)
Abstract · arxiv
AI has made remarkable progress in mathematics, solving challenging problems with machine-checkable proofs in Lean, yet typically relying on predefined mathematical definitions and formal specifications. This raises a natural question: can it reason rigorously about an unknown world? We introduce the Algebraic World Model (AWM), a framework that turns interaction with unfamiliar environments into explicit mathematical models supporting formal reasoning. AWM explores the environment and develops executable Python hypotheses, continually testing and revising them against observations. It then structures these hypotheses into typed objects and shared rules, simplifies their structure through category-theory-guided transformations, and formalizes the resulting model in Lean 4 to prove reachability and impossibility. AWM can formally prove that a goal is unreachable, even beyond explored trajectories. On two impossible game levels, it constructs closed, kernel-checked Lean proofs excluding every legal winning sequence in all six runs, while Claude Opus 5.5 and GPT-6 Astra, equipped with coding tools, produce none in twelve baseline runs. Four of AWM's six initial bounds are correct, compared with one for Opus 5.5 and none for GPT-6 Astra; given only feedback that a cheaper win exists, AWM revises its rules and constructs new proofs, reaching six of six correct bounds. Moreover, AWM produces interpretable mathematical models whose rules can be inspected and tested step by step. Across all 25 public ARC-AGI-3 games, these models enable Lean to replay the winning trajectories of all 183 levels and generalize beyond observed play, predicting unseen transitions and detecting changes in game mechanics. With Claude Opus 5, AWM clears all levels with a score of 99.9, while its certified winning trajectories use only 43% of the human baseline's actions.