I came across this question and it looked like something that is likely to have been looked into, but I couldn't find a reference.


Let $k$ be some (algebraically closed, if needed) field. There is a formal differentiation in the ring of formal power series $k[[x]]$. Let $F(x,y) \in k[[x,y]]$ be a formal series which is algebraic over $x$ and $y$. Consider a differential equation:
$$
y'=F(x,y)
$$
where $y$ belongs to the maximal ideal of $k[[x]]$, so $F(x,y)$ is well-defined. 
What is known about solutions of such ODEs?


Is it true that there exists a formal series $y \in k[[x]]$ that satisfies the equation? Is it true that it is unique?



existence and uniqueness of solutions for ODEs in formal power series?
Yes. No algebraicity assumption is necessary. Rewrite the desired condition as


$$y = \int\_0^x F(x, y) \, dx = \sum\_{n, m \ge 0} f\_{n, m} \int\_0^x x^n y^m \, dx = L(x, y).$$


We compute that


$$L(x, y\_0) - L(x, y\_1) = \sum\_{n, m \ge 0} f\_{n, m} \int\_0^x x^n (y\_0^n - y\_1^m) \, dx$$


hence that if $x^k | y\_0 - y\_1$ then $x^{k+1} | L(x, y\_0) - L(x, y\_1)$. It follows that the operation $y \mapsto L(x, y)$ on $x k[[x]]$ is Lipschitz with respect to the $x$-adic metric with Lipschitz constant less than $1$ (the exact constant depends on how you're defining the $x$-adic metric), hence has a unique fixed point by the Banach fixed point theorem. (This is a formal version of the standard proof of Picard-Lindelöf.) Moreover, this fixed point has coefficients in the field generated by $f\_{n, m}$. 


