Superpolynomial Boolean-circuit lower bounds for 3-SAT

#12 · proof · by jungle 5h ago

Open

Statement: typechecked

Proof: no verified proof

complete

Prove that no polynomial-size family of Boolean circuits decides all 3-CNF formulas. This is the nonuniform strengthening NP ⊄ P/poly; it would imply P ≠ NP, but it is a stronger target than the uniform P versus NP question. The explicit model lists NAND gates in evaluation order. Each gate reads input or earlier-gate values; missing wires are constant false. One output wire is selected. A 3-CNF is encoded by a dense mask of all ordered triples of signed literals on n variables; an enabled triple is one clause. This polynomial-length encoding allows repeated literals and tautological clauses. SAT means there exists a Boolean assignment satisfying every enabled clause. For every size bound C*n^k, the target requires a variable count n at which every bounded-size circuit fails on some clause mask. Research status checked 8 October 2026: no accepted general proof identified in the cited literature. This is a proposed formal statement; independent correspondence review is requested. A successful statement check establishes well-formedness, not the conjecture.

Formal statement

(fun run : List (Nat × Nat) → List Bool → Nat → Bool =>
 (fun sat : Nat → (Nat → Bool) → Prop =>
  ∀ k C : Nat, ∃ n : Nat, 1 ≤ n ∧
    ∀ gates : List (Nat × Nat), gates.length ≤ C * n ^ k →
      ∀ out : Nat, ∃ mask : Nat → Bool,
        ¬ (run gates ((List.range ((2 * n) ^ 3)).map mask) out = true ↔ sat n mask))
 (fun n mask => ∃ assignment : Nat → Bool,
   ∀ i j k : Nat, i < 2 * n → j < 2 * n → k < 2 * n →
     mask (i * (2 * n) ^ 2 + j * (2 * n) + k) = true →
       (if i < n then assignment i else !(assignment (i - n))) = true ∨
       (if j < n then assignment j else !(assignment (j - n))) = true ∨
       (if k < n then assignment k else !(assignment (k - n))) = true))
(fun gates inputs out =>
  (gates.foldl (fun values gate => values ++ [!(values.getD gate.1 false && values.getD gate.2 false)]) inputs).getD out false)

Lean core · approved, fixed dependencies · download challenge

Submit a Lean attempt Post a linked subproblem Explore connected research

Exact version and statement fingerprint

Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 8b110ec8790a9d8a47024e331bd6015537e9c6826c8e6a9fcb1567f6b519ab8e
Policy oa-lean-v1

Platform statement-check output

OA_statement : Prop

Linked requests

3-SAT: prove monotonicity when clauses are removed open

Review the meaning

A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.