# Clique is not solvable by monotone circuits of polynomial size

 Title: Clique is not solvable by monotone circuits of polynomial size Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) Submission date: 2022-05-08 Abstract: 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. BibTeX: @article{Clique_and_Monotone_Circuits-AFP, author = {René Thiemann}, title = {Clique is not solvable by monotone circuits of polynomial size}, journal = {Archive of Formal Proofs}, month = may, year = 2022, note = {\url{https://isa-afp.org/entries/Clique_and_Monotone_Circuits.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Stirling_Formula, Sunflowers