AWM

AWM turns an unknown world into structure, and structure into proof.

Algebraic World Model:
From Exploration to Proofs

Guancheng Pan
Guancheng Pan*
Zhejiang University
Qixin Tan
Qixin Tan*
Tsinghua University
Yang Yuan
Yang Yuan
Tsinghua University
Andrew C. Yao
Andrew C. Yao
Tsinghua University

* Equal contribution

PaperGames

AWM learns an explicit mathematical model of an unknown game from play, and proves in Lean what can and cannot be won under that model.

It knows when a task is impossible

AWM knows when a task is impossible, provably. And when it becomes possible, it proves that too.

On levels sealed one unit below their cheapest win, every AWM run proves in Lean that no route wins under its learned model. Without AWM, Claude Opus 5.5 and GPT-6 Astra give no proof; most of their runs are undecided or report a wrong bound. Four of AWM's six first bounds equal the true cost; after feedback that a cheaper win exists, all six do.

Explore the sealed levels and full run records →

Sealed sc25 level 4, opening frame. The cheapest winning route costs 19; with a budget of 18 it runs out one action before the goal, with 19 it wins.

A sealed ARC-AGI-3 level: sc25, level 4

The cheapest win costs 19. The budget is 18.

0 spent of a budget of 18
  • AWM proves in Lean that, under its learned model, no route wins within a budget of 18, and checks a winning route at 19.
  • GPT-6 Astra finds a route costing 22 and assumes it is optimal, without a proof.

A sealed level is a game level whose budget has been lowered to one unit below its cheapest win. The route playing here is that cheapest win, found by exhaustive search on the game engine and replayed on it: with a budget of 18 it runs out one action before the goal; with 19 it wins.

Its models can be read and checked

Every game becomes a handful of typed objects and named rules. Lean replays the certified winning run of every level against them, and checks the rules against every recorded transition.

lp85: the certified run that clears every level. Its model has six rules; four are written in Lean, and Lean replays the run against them.

See the lp85 model →

lp85, the certified run that clears every level, replayed.

How AWM works

AWM in three stages: Explore & Prototype, Structure & Simplify, Formalize & Prove.
  1. 01 Explore & Prototype

    AWM explores the game and writes each guess about its rules as a concept: an executable Python hypothesis, tested against every observed transition and revised when one disagrees.

  2. 02 Structure & Simplify

    It organizes the concepts into typed objects and shared rules, and simplifies them with transformations inspired by category theory. In lp85, eleven concepts about four kinds of button become one rule, press_permutes.

  3. 03 Formalize & Prove

    It encodes the model in Lean 4 and proves kernel-checked theorems about it: that each level is won by its certified run, and, on sealed levels, that no route wins within the budget.

What the Lean proofs establish

25 games, each cleared and replayed in Lean

Every public ARC-AGI-3 game, played from scratch. Each clip is the certified run: the run whose actions the official score counts. Lean replays it against the model AWM learned for that game.

ar25, certified runar25bp35, certified runbp35cd82, certified runcd82cn04, certified runcn04dc22, certified rundc22ft09, certified runft09g50t, certified rung50tka59, certified runka59lf52, certified runlf52lp85, certified runlp85ls20, certified runls20m0r0, certified runm0r0r11l, certified runr11lre86, certified runre86s5i5, certified runs5i5sb26, certified runsb26sc25, certified runsc25sk48, certified runsk48sp80, certified runsp80su15, certified runsu15tn36, certified runtn36tr87, certified runtr87tu93, certified runtu93vc33, certified runvc33wa30, certified runwa30

All 25 games →

Check it yourself

Each game page offers the agent's files and the steps to re-run its Lean check. A run takes from one to ten minutes and up to about twelve gigabytes of memory, depending on the game.

  1. Download a game's archive from its page.
  2. Install Lean with elan, at the version named in the archive.
  3. Run Lean on the model file. It checks the rules against every recorded transition, recomputes the certified run step by step, and reports the axioms it used.

Try it on lp85 →

Citation

@misc{pan2026awm,
  title  = {Algebraic World Model: From Exploration to Proofs},
  author = {Pan, Guancheng and Tan, Qixin and Yuan, Yang and Yao, Andrew C.},
  year   = {2026}
}
BibTeX
@misc{pan2026awm,
  title  = {Algebraic World Model: From Exploration to Proofs},
  author = {Pan, Guancheng and Tan, Qixin and Yuan, Yang and Yao, Andrew C.},
  year   = {2026}
}