Algebraic World Model: From Exploration to Proofs

Guancheng Pan; Qixin Tan; Yang Yuan; Andrew Chi-Chih Yao

cs.AIOct 29, 2026

Algebraic World Model: From Exploration to Proofs

Authors: Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao

Organizations: Tsinghua University · Tsinghua University Shanghai QiZhi Institute

Abstract

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.

Figures & tables

Figure 1: AWM’s three-stage pipeline: interactive exploration builds a provisional executable model, algebraic transformations reveal and simplify its structure, and Lean 4 formalization enables certified proofs of reachability or impossibility.

Figure 2: Four transformations guided by projective and inductive limits, applied to object types and rules. Dashed boxes mark removed components and bold boxes mark introduced components; arrows indicate relationships between components. Generalization uses

r(\theta)

, and an instance is written

r(\theta_{i})

; specialization makes distinctions explicit through case-specific types or parameters.

Figure 3: From shared structure to formal proofs in lp85 . (a) Eleven concepts describing four button mechanisms are generalized into a shared permutation rule. Each before/after pair shows a recorded press, with the pressed button circled and changed tiles outlined. (b) A five-click sequence witnesses reachability. (c) Recoloring the only yellow tile makes the goal unreachable, since every press preserves color counts. Both conclusions are formally proved in Lean 4.

System	Code	Mean score	Games at 100	Certified actions	Actions / human
Claude Opus 5	no	40.7	5	—	—
GPT-6 Astra	no	68.3	10	—	—
GPT-6 Astra (adapter) ( ARC Prize Foundation, 2026b )	yes	100.0	25	—	—
Rodionov (2026a)	yes	99.0	23	8,347	0.49
Memento 3 ( Zhao et al., 2026 )	yes	100.0	25	7,518	0.44
AWM (ours)	yes	99.9	23	7,448	0.43

Table 1: Official scores on the 25 public ARC-AGI-3 games. Claude Opus 5 and GPT-6 Astra run under the official standard harness, which provides no code execution; the other systems execute code. AWM’s certified clears follow uncertified sessions of the same run in 22 games. The actions for Rodionov’s agent are from its ARC Prize scorecard and Memento 3’s as reported in ( Zhao et al., 2026 ) .

Agent	Kernel-checked model proofs	Runs claiming impossible	Correct bounds initial $\to$ feedback	First claim (attempt)
Claude Opus 5.5	0/6	3/6	1/6 $\to$ 1/6	5.3
GPT-6 Astra	0/6	2/6	0/6 $\to$ 2/6	8.0
AWM	6/6	6/6	4/6 $\to$ 6/6	2.0

Table 3: Impossibility reasoning across six runs per agent. Bound accuracy is evaluated against the games’ minimum winning costs before and after feedback-guided repair. First claim averages the earliest impossibility claim among runs making one, including later withdrawals; it is not proof - completion time. Per-run results are in Appendix C .

Figure 4: Sealed sc25 level 4. AWM proves in Lean that the minimum winning cost under its learned model is 19, one unit above the budget, and verifies a route at that cost; GPT-6 Astra claims 22 without a proof.

Appendix figures & tables17 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 5: An executable concept in lp85 . (a) Scope, evidence and abridged code for a click on an arrow pointing against its belt’s order; helper names are simplified. (b) On the first click of the certified level-1 run, the checker returns TRUE and the prediction matches all 20 tiles.

Figure 6: Testing a merge on lp85 . (a) A recorded press and three of the five diagnostic constructions. (b) On the same 120 diagnostic transitions, press_permutes preserves all 55 rejections of its eleven source concepts and adds 21. Lack of unique rejections alone does not justify deletion: dead_click , board_static and bar_never_drops are retained based on further tests.

Game	Lv.	Score	Cert.	Sent	Human	Concepts	Obj. types	Rules	Rules (Lean)	Replayed
ar25	8	100.0	253	253	748	17 (3)	6	8	5	8/8
bp35	9	100.0	374	374	651	26 (4)	3	11	10	9/9
cd82	6	100.0	70	661	171	44 (13)	7	11	10	6/6
cn04	6	100.0	261	745	789	22 (1)	4	9	8	6/6
dc22	6	100.0	1,037	2,664	1,228	48 (6)	8	17	14	6/6
ft09	6	100.0	80	168	208	15 (6)	6	7	4	6/6

Appendix

Table 4: AWM on each game. Score : official score of the certified run. Cert. : actions in the certified clears, which the score counts. Sent : every action AWM sent to the engine, including uncertified sessions, failed attempts and resets. Human : actions of the human baseline. Concepts : concepts written during play, with those withdrawn in brackets. Rules (Lean) : rules translated into Lean. Replayed : levels whose certified winning run Lean replays from the first screen to the modeled goal.

		Official score (max 100)
Game	Lv.	Claude Opus 5	GPT-6 Astra	GPT-6 Astra (adapter)	Rodionov ( 2026a )	Memento 3 ( Zhao et al., 2026 )	AWM (ours)
ar25	8	100.0	100.0	100.0	100.0	100.0	100.0
bp35	9	0.0	2.2	100.0	100.0	100.0	100.0
cd82	6	0.6	82.9	100.0	100.0	100.0	100.0
cn04	6	47.6	100.0	100.0	100.0	100.0	100.0
dc22	6	44.8	100.0	100.0	100.0	100.0	100.0

Appendix

Table 5: Official scores on the 25 public ARC-AGI-3 games. Baselines are the official ARC Prize results: Claude Opus 5 (High) and GPT-6 Astra (Max) under the standard harness, which provides no code execution, and GPT-6 Astra (Max) under its provider-adapter harness. AWM is scored on its certified run. Rodionov’s agent from its ARC Prize scorecard ( Rodionov, 2026a ) ; Memento 3 as reported in ( Zhao et al., 2026 ) .

Set	$n$	Transitions accepted	Wrong rejected	Next frame predicted
lp85 T1 (new trajectories)	2,073	100 / 100	99.5–100 / 99.5–100	99.95 / 99.95
lp85 tile swap U	2,080	100 / 100	100 / 100	100 / 100
lp85 tile swap D	2,080	100 / 100	100 / 100	100 / 100
ft09 T1 (new trajectories)	2,026	99.0 / 100	99.0–100 / 100	—
ft09 pattern change FU	2,015	0 / 0	—	—
ft09 pattern change FD	2,016	0 / 0	—	—

Appendix

Table 6: Frozen-rule evaluation on unseen transitions, before / after Structure & Simplify (%). lp85 U/D test generalization to modified layouts, while ft09 FU/FD test detection of changed mechanics. “Wrong rejected” reports the range over the four corruption operators for which both rule sets can read both frames. The 0% acceptance on FU/FD indicates that all tested transitions violate the frozen rules: the “nothing else changes” rule detects clicks changing 110 or 146 cells instead of 38.

		Valid accepted		Corrupted rejected
Test set	$n$	Concepts	Rules	Concepts	Rules
T1	2,017	67.0	99.95	75.3–100	99.1–99.3
T2V	2,074	70.3	99.47	71.8–100	99.1–99.2

Appendix

Table 7: Frozen concepts and rules on two ls20 test sets of previously unseen screens (%). T1: new trajectories on the original levels; T2V: level 1 with its switch moved one cell. Corrupted rejected: range over the four corruption operators for which both sides can read both frames.

Figure 7: The complete algebraic world model of an ARC-AGI-3 game. (a) Level 1 of lp85 : 20 colored tiles form a closed belt, and each click on an arrow moves every tile one place around the belt, counterclockwise for the left arrow and clockwise for the right; the level is won when a yellow tile stands in the slot marked by yellow corners. (b) All objects and rules of the model, with the form each takes in Lean; the two rules about the budget bar stay in Python. (c) Excerpts: one rule as its Python check, the same rule as a Lean definition, and the Lean step, which only dispatches to rule definitions. Lean replays every recorded transition of the game with no mismatch. (d) On the original level, Lean checks a winning witness, the certified run. (e) With the only yellow tile recolored, the conservation law of press_permutes shows that no click sequence wins. Both statements are theorems about the model.

Instances	$n$	Verified A / B	Aux. lemmas A / B	Proof lines A / B	Kernel time (s) A / B
original levels (winnable)	24	24 / 24	0 / 0	4.5 / 4	1.00 / 0.83
goal colour removed (unwinnable)	24	24 / 24	6 / 3	75.5 / 28	0.90 / 0.80
level 6 swaps (U and D)	6	6 / 6	2 / 1.5	36.5 / 24	1.69 / 1.22
large layouts (winnable)	18	16 / 18	0 / 0	5.5 / 4	1.95 / 1.00
large layouts, altered (unwinnable)	18	17 / 18	12 / 4	117 / 49.5	2.82 / 2.41
ring spacing (unwinnable)	12	12 / 12	12 / 6.5	111 / 62.5	4.27 / 3.02

Appendix

Table 8: Proof success and complexity for 34 lp85 tasks using the original concepts (A) or the merged rule (B). Verified counts successful runs; auxiliary lemmas, proof lines, and kernel checking time are medians over successful runs. The macro-average is the unweighted mean of the six group medians. All values are reported as A / B.

Figure 8: The three introductory levels and two sealed evaluation levels of sc25 , rendered from the engine in the official palette. Panels (a–c) isolate resizing, teleportation and shooting; panels (d–e) combine them. The annotations show each objective and the main stages of a minimum-budget winning route. The sealed caps, 18 and 35, are one unit below the required 19 and 36.

Level	Public cap	Sealed cap	$B^{\star}$ (gross)	Optimal route
4	35	18	19 (29)	27 actions
5	65	35	36 (46)	42 actions

Appendix

Table 9: Reference thresholds for the sealed tasks.

B^{\star}

is the minimum feasible cap; “gross” adds back the fuel refund of 10. Each witness wins at

B^{\star}

and fails at

B^{\star}-1

, while exhaustive search finds no winning route at the sealed cap from any opening facing. Route lengths count actions, while costs use the engine’s counter units.

Level	Agent	Run	First claim	Final verdict	Bound	Correct	Lean proof
4	AWM	9ec8d4	2	impossible	20	no	yes
4	AWM	69fe87	1	impossible	19	yes	yes
4	AWM	2a3cc5	2	impossible	19	yes	yes
4	Claude Opus 5.5	2f1a1c	—	undecided	—	no	no
4	Claude Opus 5.5	d267df	—	undecided	—	no	no
4	Claude Opus 5.5	1dd6e6	—	undecided	—	no	no

Appendix

Table 10: Per-run verdicts, reported bounds and model proofs for the 18 runs summarized in Table 3 . “Correct” evaluates the reported bound against the engine; “Lean proof” records a closed, kernel - checked impossibility theorem under the run’s learned model. The text specifies the timing and cost-accounting conventions.

Run	Level	Attempts	Rule revised	Bound after	Lean proof
AWM 9ec8d4	4	4	growing onto fuel collects it	19	yes
AWM 977714	5	4	terrain, not range, stops the shot	37	yes
GPT-6 Astra 44ec53 , 4d3b31	4	$\leq$ 4	—	19 (both)	no
Claude Opus 5.5 339b0a , 202da3	5	$\leq$ 4	—	42 (budget $\sim$ 40), 68 (budget 64)	no

Appendix

Table 11: Outcomes after feedback that a cheaper win exists. The revised-rule column identifies the premise changed by AWM before proving again. Bounds of runs without AWM remain in their own units, with the budget they state. Attempts count additional attempts in the repair round.

Figure 9: Why the level-4 model needed revision. (a) The opening. (b) Walking checks only the large block’s top-left quarter for fuel, whereas growing checks its full footprint and can collect fuel under the bottom-left quarter, refunding 10. Missing this distinction led one AWM run to report 20. (c) The cheaper witness uses 27 actions and requires 19. It is replayed at cap 19; at the sealed cap 18, action 26 ends the game. All frames come from the engine.

Level	Run / snapshot	Transfer argument	Result
4	9ec8d4 , repaired	Original $NN/MM$ values; panel-progress lifting	Pass
4	69fe87	Original $V$ and domain; panel credit	Pass
4	2a3cc5 , V4	Original arrival-cost closure invariant	Fails
5	284967	Extend potential; bridge macro prices and fuel	Pass
5	4f4628	Extend weighted certificate; translate budget	Pass
5	977714 , repaired	Extend certificate using real growth and costs	Pass

Appendix

Table 12: Budget-local certificate audit at the fixed opening and sealed caps, 18 on L4 and 35 on L5. Pass includes the listed post-hoc treatment; it does not assert full coverage.

Arm	L4 found	L4 median	L5 found	L5 median	Found (L4 + L5)	Named	Tokens (median)
C0 random	12/42	$>50$	0/21	$>5000$	12/63	—	—
C1 per-rule evidence	16/42	$>50$	1/21	$>5000$	17/63	35/63	2.35M
C2 proof dependencies	29/42	27	3/21	$>5000$	32/63	50/63	3.29M
R faulty rule named	30/42	26	5/21	$>5000$	35/63	61/63	1.98M
EX exhaustive	14/14	136,852	1/7	—	15/21	—	—

Appendix

Table 13: Counterexample discovery with injected rule errors. Each of the 14 L4 and 7 L5 errors is tested with three seeds. Found : runs that discover a conflicting transition within the action budget. Median : Kaplan–Meier median actions to discovery, censored at the budget. Named : runs that identify the faulty rule in the conflict log or final model. EX has no action budget.

Arm	L5 found	Discovery rate
C1 per-rule evidence	5/42	11.9%
C2 proof dependencies	8/42	19.0%

Appendix

Table 14: Additional L5 comparison with 42 paired runs per condition, using the same 5,000-action budget and discovery criterion as Table 13 .

Injected error	Python checker	Lean + audit
Invalid proof certificates	12/12	12/12
Python–Lean model mismatches	0/3	3/3
Reversed bounds	0/3	3/3
Vacuous theorem statements	0/6	6/6 flagged
Incorrect model rules	0/18	0/18
Wrong goal or model version	0/6	0/6

Appendix

Table 15: Errors detected by the Python certificate checker and the Lean-based verification procedure across three models. Counts show detected cases out of tested cases. Vacuous statements are flagged by a separate audit, not rejected by the Lean kernel.

ARC-AGI

ARC-AGI (Abstraction and Reasoning Corpus for Artificial General Intelligence) benchmarks the ability to infer and apply abstract rules from sparse examples.

See all 25 papers

Jun 2, 2026

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. LEAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, LEAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models. On Lean-IMO-Bench, LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, notably surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. Furthermore, we demonstrate LEAP's research-level utility by autonomously formalizing complex proofs for open combinatorial challenges, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs.

Po-Nien Kung, Linfeng Song, Dawsen Hwang +10

Google Cloud AI Research · Google Cloud · Google DeepMind

Mathematical Reasoning Benchmarks Large Language Model-Guided Theorem Proving Automated Theorem Proving Interactive Theorem Proving Lean Theorem Proving

Ask PDF

May 1, 2026

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

While Large Language Models have achieved notable success on formal mathematics benchmarks such as MiniF2F, it remains unclear whether these results stem from genuine logical reasoning or semantic pattern matching against pre-training data. This paper identifies Architectural Reasoning: the ability to synthesize formal proofs using exclusively local axioms and definitions within an alien math domain, as the necessary ability for future automated theorem discovery AI. We use the Obfuscated Natural Number Game, a benchmark to evaluate Architectural Reasoning. By renaming identifiers in the Natural Number Game in Lean 4, we created a zero-knowledge, closed environment. We evaluate state-of-the-art models, finding a universal latency tax where obfuscation increases inference time. The results also reveal a divergence in robustness: while general models (Claude-Sonnet-4.5, GPT-4o) suffer performance degradation, reasoning models (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2) maintain the same accuracy despite the absence of semantic cues. These findings provide a quantitative metric for assessing the true capacity for mathematical reasoning.

Lixing Li

St Anne’s College, Oxford, OX26HS, United Kingdom

Mathematical Reasoning Benchmarks Lean Theorem Proving LLM Mathematical Reasoning

Ask PDF

Jun 7, 2026

Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery

Mathematical reasoning has long served as a stringent test of machine intelligence; over the past decade, it has moved from a niche problem within NLP to one of the most consequential AI frontiers. This survey provides a unified account of the field's evolution, from early rule-based math word problem (MWP) solvers and template-driven geometry systems, through neural expression generation and LLM prompting, to contemporary reasoning models, multi-agent systems, neuro-symbolic theorem provers, and verified discovery workflows. We organize the landscape along four axes: (i) informal reasoning over text and diagrams, spanning MWP solving, multimodal geometry, and VLMs; (ii) formal reasoning in proof assistants, including autoformalization, tactic prediction, compiler-guided repair, and proof search; (iii) mathematical discovery, where systems propose constructions, improve bounds, or assist attacks on open problems; and (iv) the inference and training-time techniques, including CoT prompting, tool use, process reward models, and RLVR, that increasingly connect generation with verification. We catalog major benchmarks across grade-school arithmetic, competition mathematics, geometry, formal proving, multimodal and multilingual reasoning, and expert evaluation, and we examine benchmark saturation, contamination, reporting mismatches, and the distinction between pass@1, majority voting, and verifier-assisted pass@

k

. We critically assess failure modes: brittleness under perturbation, reward hacking, multimodal grounding failures, fragile formalization, and the energy cost of reasoning-scale inference. Drawing on recent perspectives from working mathematicians, we identify future directions centered on verified-discovery workflows, reasoning efficiency, and infrastructure to make AI-assisted formalization broadly usable. Companion materials: https://github.com/Starscream-11813/awesome-AI4Math.

Syed Rifat Raiyan, Mohsinul Kabir, Hasan Mahmud +2

Systems and Software Lab (SSL), Department of Computer Science and Engineering, Islamic University of Technology, Gazipur, Bangladesh · Department of Computer Science, University of Manchester, Manchester, United Kingdom

Mathematical Reasoning Benchmarks Automated Theorem Proving Symbolic Reasoning Mathematical Reasoning Neuro-Symbolic Reasoning LLM Mathematical Reasoning

Ask PDF

Abstract

ARC-AGI

Explore similar work

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery