I've seen the following theorem attributed to Lurie:
Theorem. There is an equivalence of $(\infty,1)$-categories between $E_n$ algebras and locally constant factorization algebra on $\mathbf{R}^n$.
And the reference is usually given as Lurie's Higher Algebra. However it's a 1500+ pages book and search for "factorization algebra" doesn't have a match.
Can anyone give me a pointer to where exactly this is proved in Higher Algebra, or in some other books? Thanks.
The result in question is a corollary to proposition 5.4.5.15 in Higher Algebra
Theorem 5.4.5.9. Let $M$ be a manifold and let $C^⊗$ be an $∞$-operad. Composition with the map $$\mathrm{Disk}(M)^⊗ → \mathbb{E}_M^⊗$$ of Remark 5.4.5.8 induces a fully faithful embedding $$θ:\mathrm{Alg}_{\mathbb{E}_M}(C) → \mathrm{Alg}_{\mathrm{Disk}(M)}(C)\,.$$ The essential image of $θ$ is the full subcategory of $\mathrm{Alg}_{\mathrm{Disk}(M)}(C)$ spanned by the locally constant $\mathrm{Disk}(M)^⊗$-algebra objects of $C$.
When $M=\mathbb{R}^n$, the $\infty$-operad $\mathbb{E}_M$ is just the $\mathbb{E}_n$-operad.
Be careful that the book does not use the language of factorization algebras, but if you compare the definitions you'll see that there is a conservative functor from locally constant factorization algebras on $M$ to locally constant $\mathrm{Disk}(M)$-algebras such that the functor in theorem 5.4.5.9 factors as $$\mathrm{Alg}_{\mathbb{E}_M}(C)→\mathrm{Fact}^{lc}_M(C)→\mathrm{Alg}_{\mathrm{Disk}(M)}(C)$$ where the middle term is the $\infty$-category of locally constant factorization algebras and the first arrow is the one given by taking factorization homology. This, plus the existence of the "global sections" functor $\mathrm{Fact}^{lc}_M(C)→\mathrm{Alg}_{\mathbb{E}_M}(C)$ is enough to conclude the result you're after.
