Are algebras of smooth functions formally smooth? Let $M$ be a manifold. Then is the ring of smooth functions $C^\infty(M,\mathbb{R})$ formally smooth over $\mathbb{R}$?
If it helps, feel free to assume that $M$ is compact.

(This is not a joke question. And yes, I know about $C^\infty$-rings and topological algebras, but I'm still interested in the above as stated.)
 A: It seems $C^\infty(M;\mathbb{R})$ is not formally smooth for any positive-dimensional manifold. (The following argument came up in a discussion with Thomas Nikolaus, we later also found it in this MO question):
Let's start by discussing the case $M=\mathbb{R}$. Our strategy will be to show that $\Omega^1_{C^\infty(M;\mathbb{R})/\mathbb{R}}$ is not a projective $C^\infty(M;\mathbb{R})$-module. For a projective module $P$ over some ring $R$, different elements $x,x'\in P$ can always be separated by homomorphisms $P\to R$ (e.g. by embedding $P$ into a free module and using coordinate functions), equivalently the map $P\to P^{\vee\vee}$ into the double dual is injective. So it suffices to exhibit distinct elements of $\Omega^1_{C^\infty(M;\mathbb{R})/\mathbb{R}}$ which cannot be separated by homomorphisms to $C^\infty(M;\mathbb{R})$.
Claim 1: In $\Omega^1_{C^\infty(\mathbb{R};\mathbb{R})/\mathbb{R}}$, $de^x \neq e^x dx$. To detect this, it suffices to find a derivation $\partial: C^\infty(\mathbb{R};\mathbb{R})\to M$ with $\partial e^x \neq e^x \partial x$. Let $K$ be the fraction field of the local ring of stalks of smooth functions on $\mathbb{R}$ at $0$. Then $e^x$ and $x$ are algebraically independent in $K$,  so we may find a transcendence basis of $K$ over $\mathbb{R}$ consisting of $e^x$, $x$ and other elements $a_i$. It follows that $\Omega^1_{K/\mathbb{R}}$ is a free module on $de^x$, $dx$ and the $da_i$, in particular we find a derivation $K\to K$ taking $de^x$ to $1$ and $dx$ to $0$. Precomposing with the map $C^\infty(\mathbb{R};\mathbb{R})\to K$ yields the claim.
Claim 2: Every homomorphism $\Omega^1_{C^\infty(\mathbb{R};\mathbb{R})}\to C^\infty(\mathbb{R};\mathbb{R})$ takes $de^x$ and $e^x dx$ to the same element. Indeed, such homomorphisms correspond to derivations $C^\infty(\mathbb{R};\mathbb{R})\to C^\infty(\mathbb{R};\mathbb{R})$, which are given by smooth vector fields. But any smooth vector field $f\cdot \frac{\partial}{\partial x}$ takes $de^x$ to $f\cdot\frac{\partial}{\partial x} e^x$, and $e^x dx$ to $f\cdot e^x \frac{\partial}{\partial x} x$, which agree.
So $\Omega^1_{C^\infty(\mathbb{R};\mathbb{R})/\mathbb{R}}$ cannot be projective, and thus $C^\infty(\mathbb{R};\mathbb{R})$ is not formally smooth.
A zoomed-out version of the above argument is that the $C^\infty(M;\mathbb{R})$-linear dual of $\Omega^1_{C^\infty(M;\mathbb{R})/\mathbb{R}}$ is always vector fields, and so the double dual is always $1$-forms. Hence the above observation tells us that the map from "algebraic $1$-forms" $\Omega^1_{C^\infty(M;\mathbb{R})/\mathbb{R}}$ into its double dual identifies with the map to "smooth $1$-forms" $\Omega^1(M;\mathbb{R})$, and we have used algebraically independent functions with a linear dependence between their derivatives to show that map is not injective.
For $M=\mathbb{R}^n$, the same argument works for $de^{x_1}$ and $e^{x_1}dx_1$ with the coordinate function $x_1$. Finally, on a general manifold, take a coordinate ball around an arbitrary point, and extend the functions $e^{x_1}$, $x_1$ in any way. If $\psi$ is a function supported on our ball (and $1$ in a smaller neighbourhood of $x$), then we still have that $\psi \cdot d\widetilde{e^{x_1}}$ and $\psi\cdot \widetilde{e^{x_1}}d \widetilde{x_1}$ agree as "smooth $1$-forms", but not as "algebraic $1$-forms", as witnessed by going into the fraction field of stalks around our point.
EDIT: For a short proof that the stalks of $e^x$ and $x$ at $0$ are algebraically independent, first observe that since these are analytic functions, any polynomial relation $f(e^x,x)=0$ which holds in a neighbourhood of $0$ holds on all of $\mathbb{R}$, and in fact on all of $\mathbb{C}$. Since every nonzero $a$ is attained infinitely often as value of $e^x$, each of the polynomials $f(a,x)$ for fixed nonzero $a$ has infinitely many zeros in $x$, thus vanishes. So the coefficient polynomials in $f(y,x) = \sum g_i(y) x^i$ each have infinitely many zeros, thus vanish, and so $f=0$ as polynomial, proving algebraic independence.
EDIT2: In the zero-dimensional case, if $M$ is finite, $C^\infty(M;\mathbb{R})=\mathbb{R}^M$ is clearly formally smooth over $\mathbb{R}$. In the infinite case, they shouldn't be (following the comment by Martin Brandenburg). Indeed, a variant of the argument works. We still have that $C^\infty(M;\mathbb{R})$-valued derivations are vector fields, hence trivial. However, there exist nontrivial derivations on $\mathbb{R}^M$. Identify $M=\mathbb{N}$, fix a nonprincipal ultrafilter on $\mathbb{N}$, and let $K$ be the corresponding ultraproduct (which is automatically a field). The function $f: n\mapsto n$ is algebraically independent from $1$ in $K$, and so we find a derivation $K\to K$ taking $df$ to $1$. In particular, $df\neq 0$ in $\Omega^1_{\mathbb{R}^\mathbb{N}/\mathbb{R}}$. (If your manifolds are not second-countable, they still contain $\mathbb{N}$ as retract and you can still pull this nonzero element back.)
