2×2 matrix mortality claimed undecidable (AI-assisted, Lean)

Your AI and this story

Key facts

• Claim: mortality is undecidable for families of 5,799 distinct 2×2 integer matrices; all but one are fixed and nonsingular with determinants ±p for one fixed prime p, and the input affects only a single rank-one matrix (abstract)
• History (abstract): trivially decidable in dimension 1, undecidable for integer matrices in dimension ≥ 3 since 1970 (Paterson); ‘only the problem in dimension 2 is left open’. Known partial 2×2 results: decidable for two rational matrices (Bournez–Branicky) and for upper-triangular rational families (Bell–Potapov–Semukhin)
• Method (abstract): a counter machine is encoded so that a prime p enters the denominator of the encoded configuration where no later matrix can remove it; the rank-one matrix turns halting into reaching zero. ‘A companion formalization in the Lean proof assistant verifies the complete reduction’
• AI disclosure (PDF, ‘AI methodology’): ‘We used OpenAI Codex and Claude Code for mathematical research, proof development, manuscript preparation, and Lean 4 formalization. The investigation began in July 2026, when the authors used GPT-5.6-Sol to systematically investigate this problem … did not resolve the problem. The final proof architecture was selected by the authors and developed iteratively with AI assistance. OpenAI Codex with GPT-5.6-Sol was also used to generate a Lean formalization’
• Verification status: preprint with a Lean formalization of the reduction (the authors ‘reviewed the correspondence between the formalization and the mathematical statements’); not refereed; no comment from the decidability community found on 8 Nov (web search)