Proof that the effective/proper action is the generating functional of one-particle-irreducible (1PI) correlation functions In all text book and lecture notes that I have found, they write down the general statement
\begin{equation}
\frac{\delta^n\Gamma[\phi_{\rm cl}]}{\delta\phi_{\rm cl}(x_1)\ldots\delta\phi_{\rm cl}(x_n)}~=~-i\langle \phi(x_1)\ldots\phi(x_n)\rangle_{\rm 1PI}
\end{equation}
and they show that it is true for a couple of orders.
I heard that Coleman had a simple self contained proof for this statement (not in a recursive way), but I cannot find it. It might have been along the line of comparing to the $\hbar$ expansion but I'm not sure.
Do you know this proof? Is there a good reference for it?
Comment: Weinberg does have a full proof but it is hard and not intuitive. 
 A: If you want a proof, I suggest reading the works of people whose job it is to write proofs aka mathematicians. The main issue here is to be careful with combinatorial definitions and the handling of symmetry factors. A mathematically clean yet readable account of this combinatorial theorem is in this lecture by Pavel Etingof (see Theorem 3.10 and Proposition 3.12).
A: Weinberg, QFT 2, in Section 16.1 in a footnote 2 refers to Coleman, Aspects of Symmetry, p. 135-6, which features the $\hbar$/loop expansion. See also Refs. 3 & 4 for a similar idea. In this answer we provide a non-inductive argument along these lines. A nice feature of this argument is that we do not have to deal explicitly with pesky combinatorics and symmetry factors of individual Feynman diagrams. This is already hardwired into the formalism.
A) Let us first recall some basic facts from field theory. The classical (=$\hbar$-independent) action
$$S[\phi]~\equiv~\underbrace{\frac{1}{2}\phi^k (S_2)_{k\ell}\phi^{\ell}}_{\text{quadratic part}} + \underbrace{S_{\neq 2}[\phi]}_{\text{the rest}}, \tag{A1}$$
is the generating functional for bare vertices (and inverse bare propagator $(S_2)_{k\ell}$).
The partition function/path integral is
$$\begin{align} Z[J] ~:=~&\int \! {\cal D}\frac{\phi}{\sqrt{\hbar}}~\exp\left\{ \frac{i}{\hbar} \underbrace{\left(S[\phi]+J_k \phi^k\right)}_{=:~S_J[\phi]}\right\}\tag{A2} \cr
~\stackrel{\begin{array}{c}\text{Gauss.}\cr\text{int.}\end{array}}{\sim}&
{\rm Det}\left(\frac{1}{i} (S_2)_{mn}\right)^{-1/2}\cr
&\exp\left\{\frac{i}{\hbar} S_{\neq 2}\left[ \frac{\hbar}{i} \frac{\delta}{\delta J}\right] \right\}\cr
&\exp\left\{- \frac{i}{2\hbar} J_k (S_2^{-1})^{k\ell} J_{\ell} \right\}\tag{A3}\cr
~\stackrel{\begin{array}{c}\text{WKB}\cr\text{approx.}\end{array}}{\sim}&
{\rm Det}\left(\frac{1}{i}\frac{\delta^2 S[\phi[J]]}{\delta \phi^m \delta \phi^n}\right)^{-1/2}\cr 
&\exp\left\{ \frac{i}{\hbar}\left(S[\phi[J]]+J_k \phi^k[J]\right)\right\}\cr
&\left(1+ {\cal O}(\hbar)\right)     \tag{A4}\end{align} $$
in the stationary phase/WKB approximation $\hbar\to 0$. In eq. (A4)
$$ J_k~\approx~-\frac{\delta S[\phi]}{\delta \phi^k} \qquad \Leftrightarrow \qquad \phi^k~\approx~\phi^k[J] \tag{A5}$$
are the Euler-Lagrange (EL) equations for the quantum field $\phi^k$.
Notice in the diagram expansion (A3) how a bare vertex comes with $\hbar$-weight $=-1$; an internal bare propagator $(S_2^{-1})^{k\ell}$ comes with $\hbar$-weight $=+1$; and an external leg comes with $\hbar$-weight $=0$.
The linked cluster theorem states that the generating functional for connected diagrams is
$$ W_c[J]~=~\frac{\hbar}{i}\ln Z[J],  \tag{A6}$$
cf. e.g. this Phys.SE post. Note that the connected vacuum bubbles $W_c[J\!=\!0]=\frac{\hbar}{i}\ln Z[J\!=\!0]$ by definition is correlated to the normalization of the path integral, and hence is not physically relevant. (We allow the possibility that it is non-zero to be as general as possible.)
Next recall the $\hbar$/loop-expansion
$$ L~=~I-V+1, \tag{A7} $$
cf. my Phys.SE answer here.
The $\hbar$/loop-expansion together with eqs. (A4) & (A6) imply that the generating functional
$$ W_{c}^{\rm tree}[J]~\stackrel{(A4)+(A6)}{=}~S[\phi] + J_i \phi^i     \tag{A8}$$
for connected tree diagrams is the Legendre transformation of the classical action. Note that the EL eqs. (A5) are compatible with this.
Eqs. (A3) and (A6) yield
$$\begin{align} &W^{\rm tree}_c[J]~\stackrel{(A3)+(A6)}{=}\cr \lim_{\hbar\to 0} \frac{\hbar}{i}& \ln\left( \exp\left\{  \frac{i}{\hbar} S_{\neq 2}\left[ \frac{\hbar}{i} \frac{\delta}{\delta J}\right] \right\}  
\exp\left\{- \frac{i}{2\hbar} J_k (S_2^{-1})^{k\ell} J_{\ell} \right\} \right). \end{align}\tag{A9}$$
Notice how eq. (A9) only refers to objects in eqs. (A1) & (A8), and hence can be viewed as a consequence of them alone.
Eq. (A9) realizes the fact that given an arbitrary finite set of external source insertions, then (a sum of all possible) connected tree diagrams is (a sum of all possible) trees of bare propagators $(S_2^{-1})^{k\ell}$ and bare vertices.
Note that the one-loop square root factors in eqs. (A3) & (A4) do not affect the zero-loop/tree formula (A9) & (A8), respectively.
$\downarrow$ Table 1: Structural similarity between Sections A & B.
$$ \begin{array}{ccc} A &\leftrightarrow & B  \cr
\phi^k&\leftrightarrow & \phi_{\rm cl}^k \cr
S[\phi]&\leftrightarrow &\Gamma[\phi_{\rm cl}]\cr
\hbar&\leftrightarrow &\hbar^{\prime} \cr
Z[J]&\leftrightarrow &Z_{\Gamma}[J]\cr
W^{\rm tree}_c[J]&\leftrightarrow &W_c[J]
\end{array}$$
B) Finally let us address OP's question. Consider the effective/proper action
$$ \Gamma[\phi_{\rm cl}]~\equiv~\underbrace{\frac{1}{2}\phi_{\rm cl}^k (\Gamma_2)_{k\ell}\phi_{\rm cl}^{\ell}}_{\text{quadratic part}} + \underbrace{\Gamma_{\neq 2}[\phi_{\rm cl}]}_{\text{the rest}}.\tag{B1}$$
Unlike the classical action (A1), the effective action (B1) depends (implicitly) on Planck's reduced constant $\hbar$. We would like to make a loop-expansion wrt. a new parameter $\hbar^{\prime}$.
To this end, define a partition function/path integral
$$\begin{align} Z_{\Gamma}[J] ~:=~&\int \! {\cal D}\frac{\phi_{\rm cl}}{\sqrt{\hbar^{\prime}}}~\exp\left\{ \frac{i}{\hbar^{\prime}} \underbrace{\left(\Gamma[\phi_{\rm cl}]+J_k \phi_{\rm cl}^k\right)}_{=:~\Gamma_J[\phi_{\rm cl}]}\right\} \tag{B2}\cr
~\stackrel{\begin{array}{c}\text{Gauss.}\cr\text{int.}\end{array}}{\sim}&
{\rm Det}\left(\frac{1}{i} (\Gamma_2)_{mn}\right)^{-1/2}\cr
&\exp\left\{  \frac{i}{\hbar^{\prime}} \Gamma_{\neq 2}\left[ \frac{\hbar^{\prime}}{i} \frac{\delta}{\delta J}\right] \right\}\cr 
&\exp\left\{- \frac{i}{2\hbar^{\prime}} J_k (\Gamma_2^{-1})^{k\ell} J_{\ell} \right\}\tag{B3}\cr
~\stackrel{\begin{array}{c}\text{WKB}\cr\text{approx.}\end{array}}{\sim}&
{\rm Det}\left(\frac{1}{i}\frac{\delta^2\Gamma[\phi_{\rm cl}[J]]}{\delta \phi_{\rm cl}^m \delta \phi_{\rm cl}^n}\right)^{-1/2}\cr 
&\exp\left\{ \frac{i}{\hbar^{\prime}}\left(\Gamma[\phi_{\rm cl}[J]]+J_k \phi_{\rm cl}^k[J]\right)\right\}\cr
&\left(1+ {\cal O}(\hbar^{\prime})\right)    \tag{B4}\end{align} $$
in the stationary phase/WKB approximation $\hbar^{\prime}\to 0$. Also the EL eqs. for the effective action $\Gamma_J[\phi_{\rm cl}]$ for the classical field $\phi_{\rm cl}^k$ read
$$ J_k~\approx~-\frac{\delta \Gamma[\phi_{\rm cl}]}{\delta \phi_{\rm cl}^k} \qquad \Leftrightarrow \qquad \phi_{\rm cl}^k~\approx~\phi_{\rm cl}^k[J]. \tag{B5}$$
Recall that the effective action (B1) is by definition the Legendre transformation of the generating functional
$$ W_{c}[J]~\equiv~\Gamma[\phi_{\rm cl}] + J_k \phi_{\rm cl}^k   \tag{B8}$$
for connected diagrams. Note that the EL eqs. (B5) are compatible with this.
Due to the structural similarity between two the Legendre transformations (A8) & (B8), cf. Table 1, we obtain an analogue to eq. (A9):
$$\begin{align}&W_c[J]~\stackrel{(B3)+(B4)+(B8)}{=}\cr \lim_{\hbar^{\prime}\to 0} \frac{\hbar^{\prime}}{i}& \ln\left( \exp\left\{  \frac{i}{\hbar^{\prime}} \Gamma_{\neq 2}\left[ \frac{\hbar^{\prime}}{i} \frac{\delta}{\delta J}\right] \right\} \exp\left\{- \frac{i}{2\hbar^{\prime}} J_k (\Gamma_2^{-1})^{k\ell} J_{\ell} \right\} \right) .\end{align}\tag{B9}$$
In retrospect, eq. (B9) can be viewed as a functorial consequence of eqs. (B1) & (B8) alone.
On the other hand, given an arbitrary finite set of external source insertions, then (a sum of all possible) connected diagrams is (a sum of all possible) trees of full propagators$^{\dagger}$ $(\Gamma_2^{-1})^{k\ell}$ and (amputated) 1PI vertices, cf. Lemma 3.11 in Ref. 5.
Together with eq. (B9), we conclude that the effective action $\Gamma[\phi_{\rm cl}]$ is the generating functional for (amputated) 1PI vertices (and inverse full propagator $(\Gamma_2)_{k\ell}$). $\Box$
References:

*

*S. Weinberg, Quantum Theory of Fields, Vol. 2, 1995; Section 16.1.


*S. Coleman, Aspects of Symmetry, 1985; p. 135-6.


*M. Srednicki, QFT, 2007; Chapter 21. A prepublication draft PDF file is available here.


*D. Skinner, QFT in 0D, p. 32. (Hat tip: The Last Knight of Silk Road.)


*P. Etingof, Geometry & QFT, MIT 2002 online lecture notes; Sections 3.11 & 3.12. (Hat tip: Abdelmalek Abdesselam.)


*R. Kleiss, Pictures, Paths, Particles, Processes, Feynman Diagrams and All That and the Standard Model, lecture notes, 2013; section 1.5.2.
--
$^{\dagger}$ Fine print:

*

*Assume that the generator $W_c[J]$ of connected diagrams has no terms linear in $J$, so that the effective action $\Gamma[\phi_{\rm cl}]$ has no terms linear in $\phi_{\rm cl}$, and so that $(\Gamma_2^{-1})^{k\ell}=-(W_{c,2})^{k\ell}$ is the full connected propagator, cf. my Phys.SE answer here.


*Here the notion of the one-particle irreducible (1PI) vertices are defined wrt. to full propagators $(W_{c,2})^{k\ell}$, which is equivalent to the notion of 1PI vertices wrt. to bare propagators $(S_2^{-1})^{k\ell}$, cf. e.g. this Phys.SE post.
A: This has a mathematically rigorous proof using graph-related group theory. You can find it from the MIT lecture notes MATHEMATICAL IDEAS AND NOTIONS OF QUANTUM FIELD THEORY
On page 13, theorem 3.4 has the proof. To find more useful details of the proof, you can check the Cambridge lecture notes by David Skinner Advanced Quantum Field Theory. In the first chapter, he introduced the so-called $0$-dimensional quantum field theory (i.e. Gaussian integrals) and the group theory you need to understand the proof from the previous lecture notes.
