Just today I finally managed to fix the proof of “formally smooth + locally of finite presentation <=> smooth” for morphisms of algebraic spaces, see Lemma Tag 04AM. In fact, the implication “=>” isn’t hard, and is the result that is used in practice. In the current implementation, the proof of “<=” uses infinitesimal deformation of maps, and in particular a topos theoretic description of first order thickenings of algebraic spaces which we alluded to in this post, see Lemma Tag 05ZN and Lemma Tag 05ZN.

Here is a related fact:

Suppose that X —> Y —> Z are morphisms of algebraic spaces or schemes, that X —> Y is etale and that X —> Z is formally smooth. Then Y —> Z is formally smooth too. 

In other words, being formally smooth is etale local on the source and target. See Lemma Tag 061K for a more precise statement.

If X, Y, Z are schemes, then one can prove this by reducing to the affine case, using that formal smoothness is equivalent to the cotangent complex being a projective module in degree 0 [Edit 5/18/2011: Wrong! See here.], and using the distinguished triangle of cotangent complexes associated to a pair of compose-able ring maps.

If X, Y, Z are algebraic spaces, then one has to do a bit more work (I think). The proof of the reference above uses the material mentioned in the first paragraph and that Ω_{X/Z} is a locally projective, quasi-coherent O_X-module (see Lemma Tag 061I), which is fun in and of itself.