Let $X$ be a regular scheme (all local rings are regular). Let $Y,Z$ be two closed subschemes defined by ideals sheaves $\mathcal I,\mathcal J$. Serre gave a beautiful formula to count the intersection multiplicity of $Y,Z$ at a generic point $x$ of $Y\cap Z$ as:
$$\sum_{i\geq 0} (-1)^i\text{length}_{\mathcal O_{X,x}} \text{Tor}_i^{\mathcal O_{X,x}}(\mathcal O_{X,x}/\mathcal I_x, \mathcal O_{X,x}/\mathcal J_x)$$
It takes quite a bit of work to show that this is the right definition (even that the sum terminates is a non-trivial theorem of homological algebra): it is non-negative, vanishes if the dimensions don't add up correctly, positivity etc. In fact, some cases are still open as far as I know. See here for some reference.
I have heard one of the great things about Lurie's thesis is setting a framework for derived algebraic geometry. In fact, in the introduction he used Serre formula as a motivation (it is pretty clear from the formula that a "derived" setting seems natural). However, I could not find much about it aside from the intro, and Serre formula was an old flame of mine in grad school. So my (somewhat vague):
Question: Does any of the desired properties of Serre formula follow naturally from Lurie's work? If so (since things are rarely totally free in math), where did we actually pay the price (in terms of technical work to establish the foundations)? EDIT: Clark's answer below greatly clarifies and gives more historical context to my question, highly recommend!)
