# Beyond the square-root exponent for depth-three circuits

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Beyond the Square-Root Exponent for Depth-Three Boolean Circuits](../../preprints/Beyond-the-Square-Root-Exponent-for-Depth-Three-Boolean-Circuits-September-23-2026/main.pdf)

## Scope

The formalized result gives one polynomial-time Boolean language whose exact depth-three OR–AND–OR circuit size eventually exceeds $2^{A\sqrt n}$ for every fixed $A>0$. The language and its polynomial-time algorithm are fixed before $A$ is chosen, while circuits may vary with the input length. Gates have unrestricted finite fan-in and sharing, with free input negations and constants. The result does not assert a fixed exponent $n^{1/2+\varepsilon}$ or a lower bound for unrestricted depth.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Depth-three circuit lower bound beyond every square-root constant | [DepthThree.lean](../ComparatorChallenges/DepthThree.lean) |