{"id":"palomar/PALOMAR-2026-11-04-000006","url":"https://github.com/zzyzek/NaturalProof-Lean/tree/8c1df29730a2f34d3513b693a5bac5d33abe1520","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-04-000006-v1.json","repo":"https://github.com/zzyzek/NaturalProof-Lean","tags":["cs.CC","msc:68Q17","msc:68Q06"],"score":0,"title":"The natural proofs barrier (Razborov and Rudich)","trust":"high","domain":"cs.CC","source":"palomar","authors":["Z. Zzyzek (github: zzyzek)"],"reviews":0,"subject":"cs.CC","summary":"A Lean 4 proof of Theorem 4.1 of A. A. Razborov and S. Rudich, Natural proofs (1997). If a generator G_k from k bits to 2k bits, computed by circuits of polynomial size, has hardness at least 2^(k^ε) for some ε > 0 and infinitely many k, then no P/poly-natural combinatorial property is useful against P/poly. The proof follows the paper. The generator gives Goldreich–Goldwasser–Micali functions of n variables with polynomial-size circuits, which a useful property must reject. The circuit that decides the large constructive subproperty then tells these functions apart from random functions. A…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-11-04","reactions":{},"formalized":true,"formalizes":[{"title":"Natural proofs","identifier":"doi:10.1006/jcss.1997.1494","relationship":"formalizes"}]}