The natural proofs barrier (Razborov and Rudich)
Source: github.com/zzyzek/NaturalProof-Lean/tree/8c1df29730a2f34d35…
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-04-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-04-000006/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-04-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'