Lean 4 中经机器验证的自然证明障碍

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.