The paper introduces the Algebraic World Model (AWM), a framework that lets an AI explore unfamiliar environments, generate executable Python hypotheses, refine them through category‑theory guided transformations, and formalize the resulting model in Lean 4 to prove reachability and impossibility. AWM demonstrates its ability to formally prove that certain game goals are unreachable, outperforming large language models such as Claude Opus 5.5 and GPT‑6 Astra on impossible levels, and it produces interpretable mathematical models that enable Lean to replay and generalize winning trajectories across 25 public ARC‑AGI‑3 games.
By Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao
arXiv:2609.06816v1 Announce Type: new
Abstract: Decision-time search in perfect and imperfect information games with enumerable belief states are effective methods for game AI. Collectible card games...
By Dustin Rubin
arXiv:2609.00706v1 Announce Type: new
Abstract: The SAIR Mathematics Distillation Challenge on Equational Theories asks a solver to classify whether one magma identity implies another and, for either...
By Haobo Ma, Wenlin Zhang, Manuel Israel C\'azares
PokaiTrainer is a competitive Pokémon VGC agent that scales belief‑state search to handle simultaneous, large joint action spaces and stochastic outcomes. The system uses PokaiEngine, a Rust battle engine that efficiently enumerates joint action outcomes with high accuracy, and adapts Student of Games to solve each decision as a Bayesian matrix game under a compute budget. In live Showdown play, the agent achieved a 59% win rate against a human field averaging ~1320 Elo, reaching an Elo band of 1350‑1400 and briefly entering the top 500 of the format.
By Max Yu
The paper introduces Rewindable Interactive Proofs (RIPs), a new model for scalable oversight where a weak verifier can rewind a powerful AI prover to an earlier state during interaction. RIPs enable verification of oracle‑aided computations that are robust to small changes in oracle answers, achieving near‑linear verifier time without relying on cryptography. The authors provide a construction, implement it on MNIST, and demonstrate that RIPs can outperform existing proof systems in practice.
By Ziyi Guan, Yael Tauman Kalai, Ron Rothblum, Zoe Xi
The paper reports that all 1,325 theorems from the VeriContest benchmark—comprising 1,007 competitive‑programming problems in Rust with Verus specifications—were successfully proved using Rust‑Prover, a Lean 4‑based verifier. The authors translated each Verus specification and Rust program into Lean, then used Lean’s kernel to confirm the proofs, achieving a 70% first‑iteration success rate and completing 1,259 proofs in under 32 hours on Claude Opus 5.5. The translated Lean programs matched the original Rust outputs on 21,413 benchmark test cases, and the study also compared performance across multiple large‑language‑model settings, noting that higher reasoning effort increased cost without improving proof counts.
By Traian Serbanuta, Jun Xu, Andrei Stefanescu, Cosmin Radoi
arXiv:2608.21356v1 Announce Type: cross
Abstract: For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. Here we report that generative AI in...
By Jason Hickey
arXiv:2606. 06468v1 Announce Type: new Abstract: We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement.
By Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fowl, Sanjeev Arora
The paper introduces a method for certifying the quality of solutions produced by heuristic solvers for general‑sum extensive‑form games. By relating the Nash gap of a weighted average strategy to external regret and a signed correction term, the authors derive an online certificate that can be computed in linear time per checkpoint. Experiments on the biased Leduc family show that selecting the iterate with the smallest certificate from a portfolio of training‑free regret‑matching solvers achieves high success rates across multiple test sets.
By Boning Li, Longbo Huang
The paper introduces Rewindable Interactive Proofs (RIPs), a new model for scalable oversight where a weak verifier can rewind a powerful AI prover to an earlier state during interaction. RIPs enable efficient verification of computations whose outputs are robust to small changes in oracle answers, achieving near-linear verifier time without relying on cryptography. The authors implement the protocol, demonstrate a preliminary MNIST experiment, and show that an RIP can outperform a state‑of‑the‑art deployed proof system.
The paper introduces XiangqiBench, an executable benchmark for evaluating large language model agents in Chinese chess. It tracks 8,568 multi‑turn trajectories from 12 frontier LLMs, revealing that metrics such as the Conversion Gap, Consistency Gap, and Simulation Gap overstate true closed‑loop success. The study shows that simply naming the correct move is insufficient; agents must reliably carry a plan through to a verified outcome against an opponent.
By Yekun Chai, Qiwei Peng, Haoyi Xiong
arXiv:2606. 19399v1 Announce Type: cross Abstract: LLM-based formal provers often collapse rich verifier signals (syntax errors, type mismatches, partial goal progress) into a binary pass/fail bit.
By Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang