We consider exponentially large finite relational structures (with the universe {0, 1}n ) whose basic relations are computed by polynomial size (n O(1)) circuits. We study behaviour of such structures when pulled back by P/poly maps to a bigger or to a smaller universe. In particular, we prove that:
1. If there exists a P/poly map g: {0, 1}n → {0, 1}m , n < m, iterable for a proof system then a tautology (independent of g) expressing that a particular size n set is dominating in a size 2n tournament is hard for the proof system.
2. The search problem WPHP. decoding RSA or finding a collision in a hashing function can be reduced to finding a size m homogeneous subgraph in a size 22m graph.
Further we reduce the proof complexity of a concrete tautology (expressing a Ramsey property of a graph) in strong systems to the complexity of implicit proofs of implicit formulas in weak proof systems.