In algebraic geometry, the theorem on formal functions states the following:
- Let  be a proper morphism of noetherian schemes with a coherent sheaf be a proper morphism of noetherian schemes with a coherent sheaf on X. Let on X. Let be a closed subscheme of S defined by be a closed subscheme of S defined by and and formal completions with respect to formal completions with respect to and and . Then for each . Then for each the canonical (continuous) map: the canonical (continuous) map: 
 
- is an isomorphism of (topological)  -modules, where -modules, where- The left term is  . .
 
- The canonical map is one obtained by passage to limit.
 
The theorem is used to deduce some other important theorems: Stein factorization and a version of Zariski's main theorem that says that a proper birational morphism into a normal variety is an isomorphism. Some other corollaries (with the notations as above) are:
Corollary: For any  , topologically,
, topologically,
 
where the completion on the left is with respect to  .
.
Corollary: Let r be such that  for all
 for all  . Then
. Then
 
Corollay: For each  , there exists an open neighborhood U of s such that
, there exists an open neighborhood U of s such that
 
Corollary: If  , then
, then  is connected for all
 is connected for all  .
.
The theorem also leads to the Grothendieck existence theorem, which gives an equivalence between the category of coherent sheaves on a scheme and the category of coherent sheaves on its formal completion (in particular, it yields algebralizability.)
Finally, it is possible to weaken the hypothesis in the theorem; cf. Illusie. According to Illusie (pg. 204), the proof given in EGA III is due to Serre. The original proof (due to Grothendieck) was never published.