[proofplan]
The proof uses Nirenberg's smooth counterexample as the analytic input. First we recall how a rank-one complex line field on a real $3$-manifold defines a formally integrable hypersurface-type CR structure. Then we state the key property of Nirenberg's construction: the local equation $\bar L f=0$ has too few smooth solutions near the chosen point to provide embedding coordinates. Finally we observe that any local CR embedding would have component functions solving exactly this equation, with independent differentials, contradicting the arranged PDE obstruction.
[/proofplan]
[step:Realize a rank-one complex line field as a formally integrable CR structure]
Let $M$ be a smooth real $3$-manifold. A smooth hypersurface-type CR structure of CR dimension $1$ on $M$ is a smooth complex line subbundle
\begin{align*}
T^{0,1}M\subset \mathbb C TM
\end{align*}
such that
\begin{align*}
T^{0,1}M\cap \overline{T^{0,1}M}=\{0\}.
\end{align*}
Here $\mathbb C TM:=TM\otimes_{\mathbb R}\mathbb C$ denotes the complexified tangent bundle, and $\overline{T^{0,1}M}$ denotes the complex conjugate subbundle inside $\mathbb C TM$.
On a coordinate neighbourhood $U\subset M$, let
\begin{align*}
\bar L\in \Gamma(U,\mathbb C TU)
\end{align*}
be a nowhere-vanishing smooth complex vector field and set
\begin{align*}
T^{0,1}M|_U:=\operatorname{span}_{C^\infty(U;\mathbb C)}\{\bar L\}.
\end{align*}
If $a,b\in C^\infty(U;\mathbb C)$, then the bracket of the two local sections $a\bar L$ and $b\bar L$ is
\begin{align*}
[a\bar L,b\bar L]=(a\bar L(b)-b\bar L(a))\bar L.
\end{align*}
Thus
\begin{align*}
[\Gamma(T^{0,1}M),\Gamma(T^{0,1}M)]\subset \Gamma(T^{0,1}M)
\end{align*}
locally, and hence globally after checking in local generators. Therefore formal integrability is automatic for a smooth complex line distribution.
[guided]
The CR dimension is $1$, so locally the bundle $T^{0,1}M$ has one smooth complex generator. Let
\begin{align*}
\bar L\in \Gamma(U,\mathbb C TU)
\end{align*}
be such a generator over a coordinate neighbourhood $U\subset M$. This means every local section of $T^{0,1}M$ over $U$ has the form $a\bar L$ for a uniquely determined function $a\in C^\infty(U;\mathbb C)$.
To verify formal integrability, take two arbitrary local sections $a\bar L$ and $b\bar L$, where $a,b\in C^\infty(U;\mathbb C)$. The Lie bracket satisfies the Leibniz rule in each argument, so
\begin{align*}
[a\bar L,b\bar L]=(a\bar L(b)-b\bar L(a))\bar L.
\end{align*}
The coefficient $a\bar L(b)-b\bar L(a)$ is again a smooth complex-valued function on $U$. Hence the bracket is still a smooth multiple of $\bar L$, so it is a section of $T^{0,1}M|_U$.
This is the special simplification in CR dimension $1$: there is no independent second direction in which the bracket could leave the line distribution. Therefore every smooth complex line distribution satisfying
\begin{align*}
T^{0,1}M\cap \overline{T^{0,1}M}=\{0\}
\end{align*}
is formally integrable.
[/guided]
[/step]
[step:Use Nirenberg's smooth line field with too few local first integrals]
We use Nirenberg's 1973 smooth non-embeddability construction as the analytic input: there exist an open neighbourhood $U_0\subset \mathbb R^3$ of $0$ and a smooth complex vector field
\begin{align*}
\bar L\in \Gamma(U_0,\mathbb C TU_0)
\end{align*}
such that the complex line bundle
\begin{align*}
E:=\operatorname{span}_{C^\infty(U_0;\mathbb C)}\{\bar L\}
\end{align*}
satisfies
\begin{align*}
E\cap \overline E=\{0\},
\end{align*}
but the local solution space of the first-order equation
\begin{align*}
\bar L f=0
\end{align*}
has the following obstruction at $0$: for every neighbourhood $V\subset U_0$ of $0$ and every $N\in\mathbb N$, no collection of smooth functions
\begin{align*}
f_1,\dots,f_N:V\to \mathbb C
\end{align*}
satisfying $\bar L f_j=0$ for all $j\in\{1,\dots,N\}$ can define a smooth embedding
\begin{align*}
F:V\to \mathbb C^N,\qquad x\mapsto (f_1(x),\dots,f_N(x))
\end{align*}
near $0$.
This is Nirenberg's non-locally-embeddable smooth CR structure. The construction is smooth, not real-analytic; the analytic content is precisely the failure of the equation $\bar L f=0$ to admit enough independent local smooth first integrals.
[/step]
[step:Convert Nirenberg's line field into the required CR manifold]
Set
\begin{align*}
M:=U_0,\qquad p:=0,\qquad T^{0,1}M:=E.
\end{align*}
Since $U_0$ is an open subset of $\mathbb R^3$, it is a smooth real $3$-manifold. By Nirenberg's construction,
\begin{align*}
T^{0,1}M\cap \overline{T^{0,1}M}=\{0\}.
\end{align*}
By the rank-one bracket computation above,
\begin{align*}
[\Gamma(T^{0,1}M),\Gamma(T^{0,1}M)]\subset \Gamma(T^{0,1}M).
\end{align*}
Thus $(M,T^{0,1}M)$ is a smooth formally integrable abstract CR manifold of hypersurface type and CR dimension $1$.
[/step]
[step:Derive the contradiction from a hypothetical local CR embedding]
Assume, toward a contradiction, that $(M,T^{0,1}M)$ is locally CR-embeddable at $p=0$. Then there exist a neighbourhood $V\subset M$ of $0$, an integer $N\in\mathbb N$, and a smooth CR embedding
\begin{align*}
F:V\to \mathbb C^N.
\end{align*}
For each $j\in\{1,\dots,N\}$, let $\pi_j:\mathbb C^N\to\mathbb C$ denote the $j$-th coordinate projection and define the component function
\begin{align*}
F_j:V\to \mathbb C
\end{align*}
by $F_j(x):=\pi_j(F(x))$ for $x\in V$.
By definition, a smooth CR embedding is a smooth embedding whose component functions are CR functions. Therefore each component $F_j$ is a CR function. In the present local generator notation, this means
\begin{align*}
\bar L F_j=0
\end{align*}
for every $j\in\{1,\dots,N\}$. Hence the component functions $F_1,\dots,F_N$ form a collection of smooth local solutions of Nirenberg's equation $\bar L f=0$. But Nirenberg's obstruction says that no such collection can define a smooth embedding near $0$. This contradicts the assumption that $F$ is a smooth CR embedding.
Therefore the CR structure $(M,T^{0,1}M)$ is not locally CR-embeddable at $p$. This proves the theorem.
[/step]
