Mortality Problem

The mortality problem asks whether a finite set of integer matrices is mortal, meaning that some matrix product of members of the set is the zero matrix. The problem is decidable for , open for , and undecidable for (Paterson 1970, Bournez and Branicky 2002).

Suppose instead that a family of real matrices generates a finite monoid consisting of matrix products indexed by words, and let be the minimum matrix rank among the members of . The authorless "Minimum-Rank and Mortality Bounds for Finite Real Matrix Monoids" (2026) claims that there is a word such that

Here is the number of symbols in the word . If contains the zero matrix, this gives

No finiteness assumption on the indexing set is needed, and the same upper bounds are claimed for rational matrices. In the rational case, the mortality upper bound improves the earlier upper bound of Almeida and Steinberg (2009), while the corresponding upper bounds improve the upper bound of Kiefer and Ryzhikov (2026) under the hypothesis that the monoid is finite. The revision also claims that every mortal finite monoid of real matrices or rational matrices in dimension 2 has a word of length at most 4 whose matrix product is the zero matrix, and that this upper bound is sharp. Whether a polynomial upper bound in exists remains open, and the result does not apply to the unrestricted mortality problem.

The accompanying Lean development checks the stated upper bounds, including the sharp length-4 result in dimension 2. As of Sep. 10, 2026, no independent statement audit or specialist review had been reported. The released source identifies the work as AI-generated and gives GPT-6 Astra as a default attribution, while noting that runtime model provenance was not retained.