Proj construction in derived algebraic geometry The question
My question is easy to state:
Is there a Proj construction in derived geometry, that produces a derived stack from a “graded derived algebra”?
Given the vagueness of the question, you’re free to interpret derived geometry in your favourite model for affines: (E-infinity/simplicial/dg)-algebras etc.
Perhaps there’s some well-known answer. If not, below I’ll write about why I’m confused about existence of such a notion.
The struggle
A first obstacle (maybe only to me, as I am dumb) is to formulate a notion of derived graded algebras. This seems possible to do directly. It’s also maybe plausible that we can characterise such graded affine schemes as derived affine schemes that receive an action by the multiplicative group scheme, viewed as a 0-truncated derived scheme. I have not thought either of these through though, but for now let’s assume some notion of graded derived rings exist.
At this point we can use a functor-of-points approach to define a notion of Proj: either in terms of maps into invertible projective modules, or as quotient prestack by the $G_m$ action. It’s not immediate (at least to me) that in the derived setting that these approaches produce equivalent results.
A more major obstacle is that in the classical case, the way we show the functor of points for Proj is representable by a scheme is by constructing an explicit model for it by gluing affines along open subschemes. If we try to reproduce this argument in the infinity-categorical setting, these gluing diagrams requires an infinite amount of coherence data. This is much like the example outlined in introduction to DAG-XIV. Can we circumvent this by appealing to the Lurie-Artin theorem?
 A: It is instructive to look at the simplest case of Proj: that of a free module, i.e. the projective space. Lurie works these out for us quite carefully in his Spectral Algebraic Geometry tome.
Projective spaces in SAG
1. Projective space by gluing:
In Section SAG.5.4, more specifically Construction SAG.5.4.1.3, he constructs a spectral algebraic scheme $\mathbf P^n_S$, following the classical gluing construction of homogeneous coordinates. It looks a little bit more funky due to $\infty$-categorical descent requiring specification of what happends on arbitrary intersections, as opposed to the classically story where double intersections, with a compatibility on triple ones, suffice (this is the infinite coherence data for gluing alluded to in the question).
This projective space $\mathbf P^n_S$ is flat, base-changes along $S\to R$ to usual projective spaces we know and love over an ordinary ring $R$, and possess a "good theory" of Serre twisting sheaves $\mathscr O(n)$, e.g. Serre's calculation in FAC of their cohomology still holds.
Its drawbacks: $\mathbf P^n_S$ is not smooth over $\operatorname{Spec} S$ (more precisely, it is fiber-smooth and is not differentially smooth), and it does not satisfy the expected universal property in terms of line bundles (for other than classical schemes).
2. Projective space by universal property:
On the other hand, Subsection SAG.19.2.6 sees Lurie apply the Artin Representability Theorem to obtain the smooth projective space $\mathbf P^n_{\mathrm{sm}}$, that satisfies the expected universal property: a map of spectral schemes $X\to \mathbf P^n_{\mathrm{sm}}$ corresponds to a line bundle $\mathscr L$ on $X$ together with a map of quasi-coherent sheaves $\mathscr L\to\mathscr O_X^{n+1}$, which exhibits the splitting $\mathscr O^{n+1}_X\simeq \mathscr L\oplus\mathscr Q$.
To check the requirements of Artin representability, Lurie uses the already-constructed $\mathbf P^n_S$, however the two spectral schemes do not coincide. The smooth projective space is smooth over $\operatorname{Spec} S$ (i.e. differentially smooth), but it is not flat. And while $\mathscr O(-1)$ is the universal bundle on $\mathbf P^n_{\mathrm{sm}}$, the cohomology of it and its twists is not controlled by Serre's computation anymore.
3. Summary: In the world of SAG there are two notions of the projective space, each satisfying some of the nice properties of projective spaces in classical AG.
All that said, that really has nothing to do with projective spaces, but instead with affine ones: it is known that SAG admits two inequivalent notions of the affine space $\mathbf A^n$, one of which $\mathbf A^n_{\mathrm{sm}}$ is (differentially) smooth, and the other of which $\mathbf A^n_S$ is flat. The two projective spaces just correspond to using each of the two variants of affine space to build a projective one.
It is explained in Lurie's thesis how requiring the two affine lines to coincide produces DAG from SAG, hence the projective space in derived algebraic geometry (e.g. built out of simplicial commutative rings, as opposed to $\mathbb E_\infty$-rings) will be as nice as you expect.
Graded derived rings and Proj
The question asks for a good notion of a graded derived $R$-algebra, and the suggestion in the comments was to just define them as affine derived $R$-schemes with a $\mathbf G_m$-action. That works, but it is also possible to imitate the usual classical definition of graded rings:
1. Classical definition of graded rings:
A graded derived $R$-algebra is a lax symmetric monoidal functor $A:\mathbf Z\to \mathrm{Mod}_R$, where the LHS is the discrete category indexed by the integers (no non-identity morphisms) with the symmetric monoidal operation given by addition, and the RHS carries the symmetric monoidal structure of the derived relative tensor product $\otimes_R$. If we denote by $A_n$ the value of the functor $A$ on the object $n\in \mathbf Z$, then the colimit $\varinjlim A\simeq \bigoplus_{n\in \mathbf Z} A_n$ is the underlying commutative $R$-algebra. The lax symmetric monoidality translates to the usual definition of a commutative graded ring:  the map $R\to A$, picking out the unit $1\in \pi_0A$, factors through the inclusion $A_0\to A$, and the multiplication on $A$ takes $A_m\otimes_R A_n\to A_{m+n}$. Phrasing things as an $\infty$-categorical functor just brings all the necessary homotopy-coherence along for the ride.
If you wanted non-negatively graded derived $R$-algebras, you could require that $A_n\simeq 0$ for all $n$, but that amounts to the same thing as a symmetric monoidal functor $\mathbf Z_{\ge 0}\to\mathrm{Mod}_R$, everything else same as before.
The relationship with the group scheme $\mathbf G_m$ and the monoid scheme $\mathbf A^1$, alluded to in the comments to the question, come from the fact that $\mathbf G_m = \operatorname{Spec} (R[\mathbf Z])$ and $\mathbf A^1 = \operatorname{Spec} (R[\mathbf Z_{\ge 0}])$.
2. Two options for $\mathbb E_\infty$-rings:
This also gives another perspective on what "goes wrong" in SAG to produce two versions of Proj. There are two notions of a polynomial algebra over an $\mathbb E_\infty$-ring $R$: the free $R$-algebra
$$R\{t\}=\operatorname{Sym}^*_R(R)\simeq R[\coprod_n B\Sigma_n]$$
and the polynomial $R$-algebra
$$R[t] = R[\mathbf Z_{\ge 0}] = R[\coprod_n \mathrm{pt}].$$
Here $\coprod_n B\Sigma_n$, also known as the nerve of the category of finite sets with bijections, is the free $\mathbb E_\infty$-space, while its path-connected components $\mathbf Z_{\ge 0}$ only form the free commutative monoid. This leads to the two different affine lines $\mathbf A^1_{\mathrm {sm}}$ and $\mathbf A^1_S$, the difference btween $\operatorname{GL}_1$ and $\mathbf G_m$ over $\mathrm{Spec S}$, and finally to the two projective spaces. So while $\mathbf P^n_{\mathrm{sm}}$ has a universal property in terms of line bundles, i.e. $\operatorname{GL}_1$-torsors, the corresponding universal property for $\mathbf P^n_S$ would be about $\mathbf G_m$-torsors. Conversely, as the gluing construction for $\mathbf P^n_S$ starts from flat affine spaces $\mathbf A^n_S$, so would the one for $\mathbf P^n_{\mathrm{sm}}$ start from the smooth flat spaces $\mathbf A^n_{\mathrm{sm}}$. As quotient stacks, we have $\mathbf P^n_S\simeq (\mathbf A^n_S-\{0\})/\mathbf G_m$ and  $\mathbf P^n_{\mathrm{sm}}\simeq (\mathbf A^n_{\mathrm{sm}}-\{0\})/\operatorname{GL_1}$.
3. Proj: Following the above discussion, you can develop two notions of Proj in the SAG setting (both of which will coincide in the DAG setting), depending on what kind of grading you feed in, of which the two projective spaces will be examples. Either could be defined equivalently via a gluing construction (specifying the classical base-affines via homogeneous localization in the classical construction of Proj) or via quotienting by the $\mathbf G_m$- or $\mathrm{GL_1}$-action respectively.
The two constructions will agree under the usual condition on the graded derived ring $A$ (phrased purely on $\pi_0A$ as we expect) that elements in graded degree $1$ generate the irrelevant ideal. Note that this is not terrbily restrictive: even the EGA only really works with Proj in this setting.
Just to sketch where the equivalence is coming from: fixing some generators $x_1, \ldots, x_n$ for the irrelevant ideal $\pi_0(A)^+$ in degree $1$, determines an open cover $\coprod_j \operatorname{Spec}(A[x_j^{-1}])\to \operatorname{Spec} A - V(A_+)$ of the complement of the closed subsheme of $\operatorname{Spec} A$ cut out by the irrelevant ideal $A_+ =\bigoplus_{n >0} A_n$. Since all the derived rings in sight are graded, this covering map is $\mathbf G_m$-(or $\mathrm{GL_1}$- resp.)equivariant, and passes to a cover of the quotient. Identifying the quotient of $\operatorname{Spec}\big(A[x_j^{-1}]\big)$ by $\mathbf G_m$ with the spectrum of the $0$-th graded part $(A[x_j^{-1}])_0$ (which goes by the name homogeneous localization in classical AG), we recover the "gluing construction" of $\operatorname{Proj}A$ as the Cech nerve of the open cover.
