If you want to prove something is a smooth manifold, a good way to begin is to decide what its tangent spaces ought to be. So let $\gamma_s$ be a (smooth) homotopy of lazy paths, say for $s$ in $(-\epsilon,\epsilon)$. Its derivative at $s=0$ is a vector field $\xi$ along $\gamma:=\gamma_0$. This is a section of $\gamma^\ast TM$, not necessarily a "lazy" one. The vector field is to count for nothing if $\gamma_s$ is a lazy thin homotopy. So we should take the quotient of $C^\infty(\gamma^* TM)$ by the subspace $L$ of those $\xi$ which have vanishing (higher) derivatives at $0$ and $1$ and such that $\dot{\gamma_0}(t)$ and $\xi(t)$ are linearly dependent in $T_{\gamma_0(t)}M$ for all $t$.

A standard method to produce smooth charts (on path spaces in particular) is to exponentiate tangent vectors. This requires an auxiliary choice, say of a metric $g$ on $M$, so the manifold structure won't be absolutely canonical; but it may well be canonical up to diffeomorphism (strategy: define a smooth structure on the family of manifolds parametrized by the contractible manifold $Met(M)$, and show it's a smooth fibre bundle).

Well, $\gamma$ induces an $L^2$-metric on $C^\infty(\gamma^{\ast}TM)$, so we could take the orthogonal complement $L^{\perp}$ (isn't that the vector fields pointwise-orthogonal to $\dot{\gamma}$, vanishing where $\dot{\gamma}$ does?) and view that as our tangent space. That makes it a little clearer that it's a Frechet space (consider the $C^k$ norms on $L^\perp$...). Let $L^{\perp}_\epsilon$ be the vector fields in $L^\perp$ which, pointwise, have length $<\epsilon$. Assume $\epsilon$ is smaller than the injectivity radius of $g$ along $\gamma$. Then one has $Exp_g \colon L^\perp\to \mathcal{P}^1 M$ (since it defines a diffeo from $(T_{\gamma(0)}M)_{<\epsilon}$ onto its image, $\exp_g$ preserves laziness). This map is injective, and it's a reasonable candidate for a coordinate chart. Declare such charts to be our atlas, defining, as a by-product, a topology - the coarsest that makes the charts continuous.

Now you have several things to check. (I haven't - maybe it doesn't work...) One of those is that the topology is Hausdorff, so you might even want to make this into a metric space, perhaps via a Riemannian metric.

If you want to prove something is a smooth manifold, a good way to begin is to decide what its tangent spaces ought to be. So let $\gamma_s$ be a (smooth) homotopy of lazy paths, say for $s$ in $(-\epsilon,\epsilon)$. Its derivative at $s=0$ is a vector field $\xi$ along $\gamma:=\gamma_0$. This is a section of $\gamma^\ast TM$, not necessarily a "lazy" one. The vector field is to count for nothing if $\gamma_s$ is a lazy thin homotopy. So we should take the quotient of $C^\infty(\gamma^* TM)$ by the subspace $L$ of those $\xi$ which have vanishing (higher) derivatives at $0$ and $1$ and such that $\dot{\gamma}(t)$ and $\xi(t)$ are linearly dependent in $T_{\gamma(t)}M$ for all $t$.

A standard method to produce smooth charts (on path spaces in particular) is to exponentiate tangent vectors. This requires an auxiliary choice, say of a metric $g$ on $M$, so the manifold structure won't be absolutely canonical; but it may well be canonical up to diffeomorphism (strategy: define a smooth structure on the family of manifolds parametrized by the contractible manifold $Met(M)$, and show it's a smooth fibre bundle).

Well, $g$ induces an $L^2$-metric on $C^\infty(\gamma^{\ast}TM)$, so we could take the orthogonal complement $L^{\perp}$ (isn't that the vector fields pointwise-orthogonal to $\dot{\gamma}$, vanishing where $\dot{\gamma}$ does?) and view that as our tangent space. That makes it a little clearer that it's a Frechet space (consider the $C^k$ norms on $L^\perp$...). Let $L^{\perp}_\epsilon$ be the vector fields in $L^\perp$ which, pointwise, have length $<\epsilon$. Assume $\epsilon$ is smaller than the injectivity radius of $g$ along $\gamma$. Then one has $Exp_g \colon L^\perp\to \mathcal{P}^1 M$ (since it defines a diffeo from $(T_{\gamma(0)}M)_{<\epsilon}$ onto its image, $\exp_g$ preserves laziness). This map is injective, and it's a reasonable candidate for a coordinate chart. Declare such charts to be our atlas, defining, as a by-product, a topology - the coarsest that makes the charts continuous.

Now you have several things to check. (I haven't - maybe it doesn't work...) One of those is that the topology is Hausdorff, so you might even want to make this into a metric space, perhaps via a Riemannian metric.