[proofplan]
We prove first that $\mathrm{CLIQUE}$ belongs to NP by using a set of $k$ vertices as a certificate and checking all pairwise adjacencies. For NP-hardness, we give a polynomial-time many-one reduction from $3\text{-}\mathrm{SAT}$ to $\mathrm{CLIQUE}$, using the standard result that $3\text{-}\mathrm{SAT}$ is NP-complete (citing a result not yet in the wiki: $3\text{-}\mathrm{SAT}$ is NP-complete). The reduction creates one vertex for each literal occurrence in each clause and connects two vertices exactly when they come from different clauses and are not complementary literals. Satisfying assignments correspond precisely to cliques selecting one compatible literal from every clause.
[/proofplan]
[step:Verify that $\mathrm{CLIQUE}$ has polynomially checkable certificates]
Let $G = (V,E)$ be a finite simple undirected graph, and let $k \in \mathbb{N}$. A certificate for a yes-instance of $\mathrm{CLIQUE}$ is a subset $S \subseteq V$ with $|S| = k$.
The verifier first checks that every listed element of $S$ is a vertex of $G$ and that the listed vertices are distinct. It then checks, for every two-element subset $\{u,v\} \subseteq S$, whether $\{u,v\} \in E$. There are
\begin{align*}
\binom{k}{2}
\end{align*}
such pairs, and $\binom{k}{2} \leq |V|^2$ because $k \leq |V|$ for any yes-certificate. Thus the verification uses polynomially many adjacency checks in the input size. The certificate itself has length polynomial in the input size. Therefore $\mathrm{CLIQUE} \in \mathrm{NP}$.
[/step]
[step:Construct the graph associated to a $3$-CNF formula]
We reduce from $3\text{-}\mathrm{SAT}$, using the standard fact that $3\text{-}\mathrm{SAT}$ is NP-complete (citing a result not yet in the wiki: $3\text{-}\mathrm{SAT}$ is NP-complete).
Let $\varphi$ be a $3$-CNF formula with clauses $C_1,\dots,C_m$. For each clause index $i \in \{1,\dots,m\}$, write
\begin{align*}
C_i = \ell_{i1} \vee \ell_{i2} \vee \ell_{i3},
\end{align*}
where each $\ell_{ij}$ is a literal, meaning either a Boolean variable $x$ or its negation $\neg x$.
Define a finite simple undirected graph $G_\varphi = (V_\varphi,E_\varphi)$ as follows. The vertex set is
\begin{align*}
V_\varphi := \{(i,j) : 1 \leq i \leq m,\ 1 \leq j \leq 3\}.
\end{align*}
The vertex $(i,j)$ represents the literal occurrence $\ell_{ij}$ in clause $C_i$. For two distinct vertices $(i,j),(r,s) \in V_\varphi$, put an edge between them exactly when they come from different clauses and their literals are not complements:
\begin{align*}
\{(i,j),(r,s)\} \in E_\varphi \iff i \neq r \text{ and } \ell_{ij} \text{ is not the complement of } \ell_{rs}.
\end{align*}
The reduction maps $\varphi$ to the $\mathrm{CLIQUE}$ instance $(G_\varphi,m)$.
This construction creates exactly $3m$ vertices and considers at most
\begin{align*}
\binom{3m}{2}
\end{align*}
candidate edges. Checking whether two literals are complements is polynomial in the size of the formula encoding. Hence the map $\varphi \mapsto (G_\varphi,m)$ is computable in polynomial time.
[guided]
The reduction turns the task “choose one true literal from every clause without contradiction” into the graph task “choose one mutually adjacent vertex from every clause.” We define one vertex for each literal occurrence, not merely for each literal, because the same literal may appear in several clauses and each clause must contribute its own choice.
Let $\varphi$ be a $3$-CNF formula with clauses $C_1,\dots,C_m$. For each clause index $i \in \{1,\dots,m\}$, write
\begin{align*}
C_i = \ell_{i1} \vee \ell_{i2} \vee \ell_{i3},
\end{align*}
where each $\ell_{ij}$ is either a Boolean variable $x$ or the negated literal $\neg x$.
We define the graph $G_\varphi = (V_\varphi,E_\varphi)$ by
\begin{align*}
V_\varphi := \{(i,j) : 1 \leq i \leq m,\ 1 \leq j \leq 3\}.
\end{align*}
The meaning of $(i,j)$ is “select literal $\ell_{ij}$ from clause $C_i$.” We connect two distinct vertices $(i,j)$ and $(r,s)$ if and only if two conditions hold: first, $i \neq r$, so the two choices come from different clauses; second, $\ell_{ij}$ and $\ell_{rs}$ are not complementary literals. Formally,
\begin{align*}
\{(i,j),(r,s)\} \in E_\varphi \iff i \neq r \text{ and } \ell_{ij} \text{ is not the complement of } \ell_{rs}.
\end{align*}
Why exclude edges inside a single clause? Because a clique of size $m$ should represent one selected literal from each of the $m$ clauses, not multiple choices from the same clause. Why exclude complementary literals? Because no Boolean assignment can make both $x$ and $\neg x$ true.
The target instance is $(G_\varphi,m)$. The graph has $3m$ vertices, and there are at most
\begin{align*}
\binom{3m}{2}
\end{align*}
unordered pairs of vertices to inspect when forming the edge set. For each pair, checking whether the clause indices are distinct and whether the two literals are complements is polynomial in the formula size. Thus the reduction is computable in polynomial time.
[/guided]
[/step]
[step:Turn a satisfying assignment into a clique of size $m$]
Assume that $\varphi$ is satisfiable. Let
\begin{align*}
a: \{\text{variables of } \varphi\} \to \{0,1\}
\end{align*}
be a satisfying assignment, where $1$ denotes true and $0$ denotes false.
Since $a$ satisfies every clause $C_i$, for each $i \in \{1,\dots,m\}$ choose an index $j_i \in \{1,2,3\}$ such that the literal $\ell_{i j_i}$ is true under $a$. Define
\begin{align*}
S := \{(i,j_i) : 1 \leq i \leq m\} \subseteq V_\varphi.
\end{align*}
Then $|S| = m$, since the first coordinates are distinct. If $(i,j_i),(r,j_r) \in S$ are distinct, then $i \neq r$. Also, the literals $\ell_{i j_i}$ and $\ell_{r j_r}$ cannot be complements, because complementary literals cannot both be true under the same Boolean assignment. By the definition of $E_\varphi$,
\begin{align*}
\{(i,j_i),(r,j_r)\} \in E_\varphi.
\end{align*}
Thus every two distinct vertices in $S$ are adjacent, so $S$ is a clique of cardinality $m$ in $G_\varphi$.
[/step]
[step:Turn a clique of size $m$ into a satisfying assignment]
Assume that $G_\varphi$ contains a clique $K \subseteq V_\varphi$ with $|K| = m$. Because no two vertices from the same clause are adjacent, the clique $K$ contains at most one vertex with first coordinate $i$ for each $i \in \{1,\dots,m\}$. Since there are exactly $m$ clause indices and $|K|=m$, it follows that for every $i \in \{1,\dots,m\}$ there exists a unique index $j_i \in \{1,2,3\}$ such that $(i,j_i) \in K$.
The selected literals
\begin{align*}
\ell_{1j_1},\dots,\ell_{mj_m}
\end{align*}
contain no complementary pair, because every two vertices in $K$ are adjacent and edges were defined only between non-complementary literals.
Define a partial assignment $a_0$ on the variables appearing among the selected literals as follows. If the selected literal $x$ appears, set $a_0(x) := 1$. If the selected literal $\neg x$ appears, set $a_0(x) := 0$. This is well-defined because the selected literals contain no complementary pair. Extend $a_0$ arbitrarily to a total assignment
\begin{align*}
a: \{\text{variables of } \varphi\} \to \{0,1\}.
\end{align*}
For each clause $C_i$, the selected literal $\ell_{ij_i}$ belongs to $C_i$ and is true under $a$ by construction. Therefore every clause of $\varphi$ is true under $a$, so $\varphi$ is satisfiable.
[/step]
[step:Conclude NP-hardness and NP-completeness]
The construction above proves, for every $3$-CNF formula $\varphi$,
\begin{align*}
\varphi \in 3\text{-}\mathrm{SAT} \iff (G_\varphi,m) \in \mathrm{CLIQUE}.
\end{align*}
The map $\varphi \mapsto (G_\varphi,m)$ is computable in polynomial time, so this is a polynomial-time many-one reduction from $3\text{-}\mathrm{SAT}$ to $\mathrm{CLIQUE}$. Since $3\text{-}\mathrm{SAT}$ is NP-complete (citing a result not yet in the wiki: $3\text{-}\mathrm{SAT}$ is NP-complete), $\mathrm{CLIQUE}$ is NP-hard. Together with $\mathrm{CLIQUE} \in \mathrm{NP}$, proved above, this shows that $\mathrm{CLIQUE}$ is NP-complete.
[/step]