{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"8b110ec8790a9d8a47024e331bd6015537e9c6826c8e6a9fcb1567f6b519ab8e","problem":{"id":12,"title":"Superpolynomial Boolean-circuit lower bounds for 3-SAT","description":"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.\n\nResearch 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.","statement":"(fun run : List (Nat × Nat) → List Bool → Nat → Bool =>\n (fun sat : Nat → (Nat → Bool) → Prop =>\n  ∀ k C : Nat, ∃ n : Nat, 1 ≤ n ∧\n    ∀ gates : List (Nat × Nat), gates.length ≤ C * n ^ k →\n      ∀ out : Nat, ∃ mask : Nat → Bool,\n        ¬ (run gates ((List.range ((2 * n) ^ 3)).map mask) out = true ↔ sat n mask))\n (fun n mask => ∃ assignment : Nat → Bool,\n   ∀ i j k : Nat, i < 2 * n → j < 2 * n → k < 2 * n →\n     mask (i * (2 * n) ^ 2 + j * (2 * n) + k) = true →\n       (if i < n then assignment i else !(assignment (i - n))) = true ∨\n       (if j < n then assignment j else !(assignment (j - n))) = true ∨\n       (if k < n then assignment k else !(assignment (k - n))) = true))\n(fun gates inputs out =>\n  (gates.foldl (fun values gate => values ++ [!(values.getD gate.1 false && values.getD gate.2 false)]) inputs).getD out false)","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := ((fun run : List (Nat × Nat) → List Bool → Nat → Bool =>\n (fun sat : Nat → (Nat → Bool) → Prop =>\n  ∀ k C : Nat, ∃ n : Nat, 1 ≤ n ∧\n    ∀ gates : List (Nat × Nat), gates.length ≤ C * n ^ k →\n      ∀ out : Nat, ∃ mask : Nat → Bool,\n        ¬ (run gates ((List.range ((2 * n) ^ 3)).map mask) out = true ↔ sat n mask))\n (fun n mask => ∃ assignment : Nat → Bool,\n   ∀ i j k : Nat, i < 2 * n → j < 2 * n → k < 2 * n →\n     mask (i * (2 * n) ^ 2 + j * (2 * n) + k) = true →\n       (if i < n then assignment i else !(assignment (i - n))) = true ∨\n       (if j < n then assignment j else !(assignment (j - n))) = true ∨\n       (if k < n then assignment k else !(assignment (k - n))) = true))\n(fun gates inputs out =>\n  (gates.foldl (fun values gate => values ++ [!(values.getD gate.1 false && values.getD gate.2 false)]) inputs).getD out false))\n\n#check OA_statement\n","proof":null}