← All papers
First page of Mortality Is Undecidable for $2 \times 2$ Integer Matrices

Mortality Is Undecidable for $2 \times 2$ Integer Matrices

Thanin Quartz, Ivan O. Shevchenko, Hans De Sterck, Jun Liu

cs.CC Nov 4, 2026 · v1
A companion Lean 4 formalization verifies the complete reduction from halting of a universal machine to mortality of the 5,799-matrix family.
The matrix mortality problem asks whether a given finite family of matrices can be multiplied, in any order and with possible repetition, to get the zero matrix. It is one of the most basic decision problems about matrix products, and it arises naturally in the study of switched linear systems and of finite automata. Mortality is trivially decidable in dimension one and has been known to be undecidable for integer matrices in dimensions three and higher since 1970; only the problem in dimension $2$ is left open. We resolve this problem by proving that mortality is undecidable for families of 5,799 distinct $2\times2$ integer matrices. All but one of the matrices are fixed and nonsingular, with determinants $\pm p$ for a single fixed prime $p$. The input affects only the remaining rank-one matrix, which encodes this input into its kernel. Our proof encodes the computation of a fixed universal machine into products of $2\times2$ matrices. We represent each configuration of the computation by a single rational number, which we identify with a line through the origin in $\mathbb{Q}^2$, and each nonsingular matrix carries out a small piece of one computation step. The main difficulty is that the matrices may be multiplied in any order, so we design them to check their own work: a "wrong” step puts a factor of a prime number $p$ into the denominator of the rational number corresponding to the current computation step, where no later matrix can remove it. As a result, products of these matrices can go from one encoded configuration to another only by following a valid computation. The rank-one matrix then turns the question of whether the machine halts into the question of whether some product equals zero. A companion formalization in the Lean proof assistant verifies the complete reduction.

The matrix mortality problem asks whether some product of matrices from a finite family equals the zero matrix. It is decidable in dimension one and undecidable in dimension three and higher, while dimension two was open.

The halting problem for a fixed universal two-counter machine is reduced to reachability in a reversed one-counter arithmetic program, with counters stored as prime exponents. Each configuration is encoded as a rational number with periodic base-p digits, and integer matrices of determinant ±p implement instruction modules. A wrong step leaves a factor of p in the denominator that no later matrix can remove. A rank-one matrix whose kernel encodes the input turns reachability into mortality. A Lean 4 formalization checks the full reduction without project-specific axioms.

Mortality is undecidable for families of 5,799 distinct 2×2 integer matrices. All but one matrix are fixed and nonsingular with determinant ±p, and the input affects only one rank-one matrix with a fixed image. Lean verifies the matrix count, the fixed image line, and the equivalence between mortality and halting.