Solution (source code)

= Solution

Let $\mathfrak m$ be the <maximal ideal> and $k=A/\mathfrak m$ the finite <residue field>. The maximal ideal of an <Artinian local ring> is <nilpotent ideal>[nilpotent], so $\mathfrak m^r=0$ for some $r$. Every quotient
$$
\mathfrak m^j/\mathfrak m^{j+1}
$$
is both an Artinian $A$-module and a <vector space> over $k$. An Artinian vector space is finite-dimensional, hence each quotient is a <finite set>. The finite filtration
$$
A\supset\mathfrak m\supset\cdots\supset\mathfrak m^r=0
$$
therefore proves that the underlying set of $A$ is finite. This is the <Finiteness criterion for an Artinian local ring>.