Possible formal smoothness mistake in EGA EGA IV 17.1.6(i) states that formal smoothness is a source-local property. In other words, a map $X\to Y$ of schemes is formally smooth if and only if there is an open cover $U_i$ ($i\in I$) of $X$ such that each restriction $U_i\to Y$ is formally smooth.
It seems however that there is a gap in the proof. The problem is in the third paragraph on page 59 (Pub IHES v 32). The reference to (16.5.17) does not give the conclusion they need. Corollary (16.5.18) does give this conclusion, but it requires a finite presentation assumption. (So, everything is OK for smoothness instead of formal smoothness.)
Quesiton 1: Can someone give a counterexample or a complete proof of 17.1.6(i)? (My bet would be that there's a counterexample.)
I think the right way of fixing this is to change the definition of formal smoothness. Recall that a map $X\to Y$ is said to be formally smooth if for any closed immersion $X'\to Y'$ of affine schemes defined by a square-zero ideal and for map $X'\to X$ and $Y'\to Y$ making the induced square commute, there is a map $Y'\to X$ commuting with all the other maps in the diagram. I think a better definition would to require only that the map $Y'\to X$ exists locally on $Y'$. 
If I'm not mistaken, this definition has the following advantages over the old one: a) The definition of smoothness (=formally smooth and locally of finite presentation) would remain unchanged. b) It would make formal smoothness a source-local property. (Or if there is no counterexample to 17.1.16(i), then the argument with the new definition would be much easier than an argument like the one in EGA, in that it would not depend on the facts in scheme theory that the sheaf of lifts $Y'\to X$ is a torsor for a sheaf derivations and that therefore, since $Y'$ is affine, there is always a global section.) In particular, it would probably be better suited for maps of general sheaves of sets on the big Zariski topology, rather than just schemes. d) It's a general rule of thumb that, in sheaf theory, it's easier to work with local existential quantifiers than global ones.
Question 2: Does anyone know of any reason why this new definition would be bad?
 A: Let me point out the following remark made by Grothendieck in his book "Catégories Cofibreés Additives et Complexe Cotangent Relatif", 9.5.8
Please excuse my translation:
"Let $f:X \rightarrow Y$ be a morphism of schemes.  We say that $f$ is "locally formally smooth" if X can be covered by opens $X_i$ which are formally smooth over $Y$.  Evidently, if $f$ is formally smooth, then it is locally formally smooth; I don't know if the converse is true in general.  It was this which was affirmed hastily in EGA IV 17.1.6 but the proof is only valid when we assume that the relative $\Omega^1$ is of finite presentation, for example if $f$ is locally of finite type.  The Lemma 9.5.7 [loc. cit., not reproduced] implies the following criterion : the map $f$ is locally formally smooth if and only if one has $N_{X/Y} = 0$ and $\Omega^1_{X/Y}$ is "locally projective" in the following sense : one can cover $X$ by open affines $X_i$ with rings $B_i$ such that over $X_i$ the quasi-coherent module $\Omega^1_{X/Y}$ is given by a projective $B_i$ module.  We will know that this condition implies the formal smoothness of $f$ if we can show that for a commutative ring $B$, every $B$ module $N$ which is locally projective is also projective - or what amounts to the same - it satisfies $H^1(X, \operatorname{Hom}(\tilde{N}, J)) = 0$ for each quasi-coherent module $J$ on $\operatorname{Spec}(B)$."
Apparently, this local nature of projectivity was shown soon thereafter by Raynaud and Gruson ("Critéres de platitude et projectivité").  In fact I think they show that it is an fpqc local condition.  I think this implies that formal smoothness is even an étale local property.
