Can isomorphisms of schemes be constructed on formal neighborhoods? Let (A,m) be a complete local Noetherian ring and let X and Y be two schemes of finite type over A (and flat over A). Let Xn and Yn be the reductions of X and Y mod mn+1.

Question: Suppose there is a compatible system of isomorphisms between Xn and Yn (for all n). Does there necessarily exist an isomorphism between X and Y over A?

In other words, suppose the formal schemes \hat{X} and \hat{Y} are isomorphic; are X and Y isomorphic? 
Remark: The answer is `no' if we drop flatness (you can just stick an extra component over the generic fiber) or finite type (A[t] vs. A{t} = the completion of A[t]).
 A: No. Let A be k[[t]]. Let X be A^1 \setminus {-1,0,1} and Y be A^1 \setminus {1,t,-1}. In explicit equations,  X = Spec k[[t]][x, y]/y(x-1)x(x+1)-1 and Y = Spec k[[t]][x, y]/y(x-1)(x-t)(x+1)-1.
Over k[[t]]/t^{n+1}, the reductions of X and Y are isomorphic because all infinitesimal deformations of a smooth affine scheme are trivial. (See corollary 4.7 in Hartshorne's notes on deformation theory.) 
However, X and Y are not isomorphic because the two fibers over the general point are not: For any field K, if we have P_K^1 \setminus {a,b,c,d} for {a,b,c,d} \in P^1(K), then the cross ratio of a,b,c and d is a well defined element of K. In particular, this applies when K=k((t)).
A: Even if your question has a negative answer in general, it is related to Artin's approximation theorem (see Publ. IHES, vol 36), which can interpreted as follows. Let S be nice scheme (classically, the spectrum of a field or of a Dedekind domain whose field of functions is a global field, but, by Popescu's desingularisation theorem, any excellent noetherian scheme is eligible). Consider two closed immersions X<-Z->Y of S-schemes of finite type. If X=Y as formal schemes, after completion along Z, then there exist Nisnevich coverings X<-V->Y. So, locally for the Nisnevich topology, X=Y.
A: In David S.'s example, I don't see a compatible sytem of isomorphisms $X_n\to Y_n$. Here is a similar example with the required properties. 
Let $A=k[[t]]$, let $Y={\rm Spec} A[x]]$ be the affine line over $A$ and $X=Y\setminus \{ y_0 \}$, where $y_0$ is the closed point of $Y$ corresponding to the ideal $(1-tx)A[x]$ (the quotient ring is $A[1/t]=k((t))$). 
Then the canonical inclusion $X\to Y$ induces clearly a compatible system of isomorphisms $X_n\to Y_n$ 
for all $n\ge 1$ (they are actually identities), and of course $X$ is not isomorphic to $Y$. 
The reason behind is that the point $y_0$ is invisible in all the formal neighborhood of the closed fibler of $Y\to {\rm Spec } A$. 
In general, a compatible system of isomorphisms $X_n\to Y_n$ induces an isomorphism between the formal schemes $\hat{X}\to \hat{Y}$. When $X, Y$ are projective, one can use GAGA to show that this isomorphism comes from an isomorphism $X\to Y$. This gives an alternative proof to the use of ${\rm Hom}(X, Y)$. 
A: I feel like I have seen some theorem saying that this result is true for projective families, and maybe even for proper families. If anyone knows a reference, please post it.
