Formalization demonstrates a barrier for combinatorial properties in complexity, indicating implications for circuit size in boolean functions.
The natural proofs barrier (Razborov--Rudich 1997) has had no machine-verified formalization in any proof assistant. We formalize it in Lean 4: if pseudorandom function generators exist, then no natural combinatorial property is useful against P/poly. The formalization is approximately 400 lines of Lean 4 with no unresolved proof obligations. We identify definition choices that make the barrier proof mechanizable without probabilistic infrastructure and analyze why simpler alternatives fail. We also formalize the Shannon counting argument: most Boolean functions require large circuits.
No takes yet. Share an insight, caveat, or question.
Alex Li (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: