Bounds on clique-detecting circuits, in *tiny* graphs

### What is the conjecture

The question would be, for *tiny* values of $n$ and $k$:

How many NAND gates are needed to detect $k$-vertex cliques in an $n$-vertex graph?

The idea is to get bounds for, like, $n=8$ and $k=4$. This is (hopefully!) easier than resolving the
[P ?= NP](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millenium/PvsNP.lean) question.

### Prerequisites needed

To represent a circuit with unbounded-fan-in NAND gates, I found it convenient to define a trapezoidal bit array (backed by a BitVec). I don't think this should be added to MathLib, though. (And I'm not sure a BitVec is the best model for this.)

[lean-clique-nand](https://github.com/joshtburdick/lean-clique-nand) is my attempt at formalizing this. Although I plan to formalize this (by making a pull request to this repo), I'm new to Lean. (This is why I practiced, using a separate tiny repo.) Comments on this would be appreciated. Also, if someone else wants to do this, that would also be great.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-03

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reviewing the linked lean-clique-nand repository, especially its trapezoidal bit array and BitVec representation, then inspect formal-conjectures conventions around the linked Millenium/PvsNP.lean entry point. Done means adding the tiny-graph clique-detection conjecture to this repository in a suitable Lean formalization.

Written by the indexing model from the issue text.