Clique is not solvable by monotone circuits of polynomial size

Given a graph $G$ with $n$ vertices and a number $s$, the decision problem Clique asks whether $G$ contains a fully connected subgraph with $s$ vertices. For this NP-complete problem there exists a non-trivial lower bound: no monotone circuit of a size that is polynomial in $n$ can solve Clique.

This entry provides an Isabelle/HOL formalization of a concrete lower bound (the bound is ${\sqrt[7]{n}}^{\sqrt[8]{n}}$ for the fixed choice of $s=\sqrt[4]{n}$), following a proof by Gordeev.