Machine-verified proof (0 sorries, 2 axioms) that P ≠ NP via exponential circuit lower bounds for Hamiltonian Cycle. Lean 4 formalization with Mathlib. Proves SIZE(HAM_n) ≥ 2^{Ω(n)} using frontier analysis, switch blocks, cross-pattern mixing, recursive funnel magnification, continuation packets, rooted descent, and signature rigidity.
First machine-verified formalization of the natural proofs barrier (Razborov-Rudich 1997) in Lean 4. Zero sorry obligations.
CL-DIAG: Diagnosing canonicalization leakage in supervised learning under group symmetry
Código del TFG de Ingeniería Informática / Code for the Computer Science Bacherlor's Thesis
Add a description, image, and links to the circuit-complexity topic page so that developers can more easily learn about it.
To associate your repository with the circuit-complexity topic, visit your repo's landing page and select "manage topics."