The first lower bound improvement on the unrestricted circuit complexity of 3-SAT. A step towards P ≠ NP.

We establish a circuit-size lower bound of (17/7 - o(1))n for 3-SAT in the binary encoding specified in the paper, where n is the number of bits describing the formula. The bound applies to circuits with arbitrary two-input Boolean gates, unrestricted depth, and unrestricted sharing of intermediate results. It improves the elementary n - 1 lower bound and strengthens the earlier 7/3 and 12/5 results in this research line. The bound remains linear and does not resolve P versus NP. This deposit contains the main paper and companion Lean source packages for the 7/3 and 12/5 results. The 17/7 formalization is ongoing and is not included. The accompanying Lean packages do not constitute a formal verification of the 17/7 theorem. Build instructions and pinned dependencies are included in each archive. Contact: smaa4@cantab.ac.uk