This is too late, but answering might help more people. This is a toy case of the standard reduction to the artinian local case.
Here is a quick sketch of what's going on. I trust people interested in this can fill in the details on their own.
Start with a proper morphism $X\to Y$ of finite type schemes over an algebraically closed field $k$. Then to verify that the morphism is an isomorphism it suffices to verify the same for all artin local rings with residue field $k$.
To see this first reduce to the affine case on the base $Y=\operatorname{Spec}(R)$. This reduction should be clear.
Now, in fact, we can check the isomorphism by base changing to the closed points of the affine scheme $Y$. In other words we can assume that $Y$ is a local scheme with spectra $(R,m)$ and residue field $k$. See the lemma below for the general statement of this dévissage.
Now we have a proper morphism $X\to \operatorname{Spec} (R)$ and base changing this morphism along $\hat{R}:=\varprojlim_n R/m^n$ we get a morphism $\hat{X}:= X\times_R \hat{R}\to \operatorname{Spec}\hat{R}$ which, by flat descent, is an isomorphism iff $X\to \operatorname{Spec}(R)$ is.
Now we want to examine the map $\hat{X}\to \operatorname{Spec}\hat{R}$, but by formal GAGA this is an isomorphism iff it's completion in the sense of formal schemes is an isomorphism.
To be more explicit, we can further base change to $\hat{X}\times_R R/m^n\to \operatorname{Spec} R/m^n$ for each $n>0$. This datum $\{\hat{X}\times_R R/m^n\to \operatorname{Spec} R/m^n\}$ is a proper formal scheme $\mathcal{X}\to \operatorname{Spf}(\hat{R})$ and so by formal GAGA comes functorially from a unique proper scheme over $\hat{R}$. Since we already had a candidate $\hat{X}\to \operatorname{Spec}(R)$ it has to be the algebraization of $\mathcal{X}\to \operatorname{Spf}(\hat{R})$.
Now the rings $R/m^n$ are Artin local ring with residue field $k$ and so, by hypothesis, $\hat{X}\times_R R/m^n\to \operatorname{Spec} R/m^n$ is an isomorphism for each $n>0$ . As a result the morphism of formal schemes $\mathcal{X}\to \operatorname{Spf}(\hat{R})$ is an isomorphism.
Thus, by functoriality of algebraization, the map $\hat{X}\to \operatorname{Spec}\hat{R}$ is an isomorphism and, as mentioned before, so is $X\to \operatorname{Spec}(R)$.
Edit: As Alex notes below, the statement can be made quite general. The formal GAGA stuff and flat descent needs a locally noetherian hypothesis, but the spreading out statement i.e. detecting isomorphisms from closed points is quite general and I am pretty sure can be found in EGA IV$_3$ but I haven't looked yet.
The most general statement that I can prove is the following
Lemma : Let $f\colon X\to Y$ be a locally finitely presented morphism with $Y$ quasi-compact (or more generally such that each point specialises to a closed point). Then $f$ is an isomorphism iff for all closed points $y\in Y$ the base change $X\times_{Y} \mathscr{O}_{Y,y}\to \operatorname{Spec} \mathscr{O}_{Y,y}$ is an isomorphism.
Ideally one could hope to see this by saying that the map $\coprod_{y\in \operatorname{Y_{cl}} }\operatorname{Spec}\mathscr{O}_{Y,y}\to Y$ is a flat (fpqc) cover. This doesn't seem to be true in general, so here's an ad hoc proof sketch.
Proof sketch: By staring at EGA I 3.6.5, one shows that the isomorphisms $X\times_{Y} \mathscr{O}_{Y,y}\to \operatorname{Spec} \mathscr{O}_{Y,y}$ as $y$ runs through the closed points of $Y$, along with the fact that every point specialises to a closed point, imply that $f\colon X\to Y$ is bijective on points. Further, again from EGA I 3.6.5 one shows that for each $x\in X$ the canonical map $\mathscr{O}_{X,f(x)}\to \mathscr{O}_{X,x}$ is an isomorphism. The latter condition implies that the map is flat, and being locally finitely presented by hypothesis, it is open. Since it is injective on points, it is an open immersion and since it is surjective on points, it's an isomorphism.