$A$ algebra of finite type over $\mathbb{Z}$, $\mathfrak{m}$ max ideal implies $A/\mathfrak{m}$ is a finite field? Suppose $A$ is an algebra of finite type over $\mathbb{Z}$ (i.e. a finitely generated ring). If $\mathfrak{m}$ is a maximal ideal of $A$, does it follow that $A/\mathfrak{m}$ is a finite field?
 A: Yes, that's true. For the proof, it suffices to show that $K := A/{\mathfrak m}$ has positive characteristic, as then it is a finitely generated field extension of ${\mathbb F}_p$, and as such finite dimensional over ${\mathbb F}_p$ by Zariski's Lemma.
Suppose on the contrary that $\text{char}(K)=0$, so $K$ is a finitely generated - hence finite algebraic - field extension of ${\mathbb Q}$ which is moreover finitely generated as a ring. Adjoining to ${\mathbb Z}$ all coefficients of the minimal polynomials of a chosen set of generators of $K/{\mathbb Z}$ shows the existence of an $n\in{\mathbb Z}\setminus\{0\}$ such that $K$ is algebraic over ${\mathbb Z}[n^{-1}]$. This implies that $K/{\mathbb Z}[n^{-1}]$ is finite, so ${\mathbb Z}[n^{-1}]$ is a field - contradiction. $\Box$
While it (hopefully) works, I don't particularly like the argument because it's indirect.

Refined question: Is there a constructive proof of ${\mathfrak m}\cap{\mathbb Z}\neq\{0\}$ for ${\mathfrak m}\lhd{\mathbb Z}[X_1,\ldots,X_n]$ maximal?

