Gowers has recently outlined a problem, which he calls "discretized Borel determinacy," whose solution is related to proving circuit lower bounds.
Can you provide a summary of the approach that is tailored to an audience of complexity theorists?
What would it take for this approach to prove anything, including re-proving known lower bounds?
Let me give a summary of my understanding of the motivation for the approach. Be warned that I am fairly new to the concept of Borel determinacy, and not at all an expert in set theory. All mistakes are mine. Also I am not sure reading this is all that much better than reading Gowers' posts.
I think what Gowers has in mind is not a finitary analogue of the Borel determinacy theorem, but a finitary analogue of the following: Borel determinacy follows from ZFC, while determinacy of analytic games requires the existence of (essentially) measurable cardinals. I will very briefly describe what games we're talking about and what Borel determinacy is, and then I will tie this in with the approach to proving lower bounds. The very high-level idea is to consider the property "allows a finitary analogue of a proof of Borel determinacy to work" as a property that can separate P\poly from NP.
We think of games where two players I and II take turns "playing" an integer. The game goes on forever, so they produce a sequence $x= x_1, x_2, \ldots$. The game is defined by a winning set $A \subseteq \mathbb{N}^\mathbb{N}$ (i.e. a set of sequences). If $x \in A$ then player I wins, otherwise player II wins.
A game is determined if either player I or player II has a winning strategy: a way to decide a next move based on the play so far that guarantees a win. Whether all games are determined turns out to have intimate connections to the foundations of set theory (they are not, if you believe in the axiom of choice). In any case, one simple example when games are in fact determined is when $A$ is open in the product topology on $\mathbb{N}^\mathbb{N}$, which is a fancy way of saying that membership $x \in A$ can be decided based only on a finite number of elements of $x$. For example the game in which player I wins if she is the first to play an even number is open. Another simple example of determined games is closed games, i.e. games where $x \not \in A$ can be decided based on a finite subsequence of $x$. Closed games are open games with the roles of players inverted.
Now we can come to Borel determinacy, and right after I will try to tie this in with circuits and complexity. A Borel set is a set that can be derived from open and closed sets by repeatedly applying a countable number of unions and intersections. You should think of open and closed sets as your basic sets, and Borel sets as derived from basic sets using several levels of a "small" (= countable) number of simple operations in each level. It turns out that you can prove in ZFC that Borel sets are determined, and there is a precise sense in which this is the best you can do.
The analogy that I think Gowers is drawing here is that Borel sets are like small circuits. In the finite world, we replace the "universe" $\mathbb{N}^\mathbb{N}$ by the hypercube $\{0,1\}^n$. Our basic sets become facets of the cube: $\{x \in \{0,1\}^n: x_i = b\}$ for $b \in \{0,1\}$; these are equivalent to literals $x_i$ and $\bar{x}_i$. You can write AND and OR of literals as unions and intersections of such sets. So, for a boolean functions $f:\{0,1\}^n \rightarrow \{0,1\}$, being able to produce $f^{-1}(1)$ out of $s$ unions and intersections of basic sets is equivalent to having a size $s$ circuit for $f$.
Let me throw a word in about analytic sets. An analytic set is a projection of a Borel set: if $S \subseteq X \times Y$ is a Borel set, then $T = \{x: \exists y\ (x,y) \in S\}$ is analytic. By our correspondence between Borel sets and functions of small circuit complexity, analytic sets are like NP/poly.
Now he draws inspiration from a proof of Borel determinacy to come up with a property (in the Razborov-Rudich sense) to distinguish functions of small circuit complexity from functions of large circuit complexity. The hope of course is that the property avoids the natural proofs barrier.
Martin's proof of Borel determinacy uses a conceptually very neat approach: Martin shows that every Borel game is a the image of an open (in fact clopen) game under a map $\pi$, so that $\pi$ preserves winning strategies -- let's call this a "lift". So what Martin shows is that each Borel game is the image of a game in which the winning set is a basic set. Since open games are easily seen to be determined, this proves Borel determinacy. The proof is inductive, with the base case showing that closed games can be lifted. The important part is that each step of the induction "blows" up the universe: getting rid of one level of the Borel set construction requires lifting a game to a game over a universe that is essentially the power set of the universe of the original game. Interestingly, this is unavoidable: Borel sets that require more levels to define can only be lifted to games over much larger universes. Analytic sets require universes that are so large, that their existence requires large cardinal axioms.
Drawing inspiration from this, Gowers formulates a game in which player I and player II must jointly specify some $x$; player I wins if $f(x) = 1$, otherwise player II wins. Player I can specify the first half of the coordinates, and player II the second half. The intuition now is that games corresponding to simple $f$, i.e. $f$ with small circuit complexity, should allow a Martin-style lift to a relatively small universe, just like Borel games do. On the other hand random $f$ should require double exponential size universes, and hopefully NP-hard $f$ should as well, because they would correspond to analytic games.
Let me be just slightly more concrete about what a Martin-style lift is, but do check Gowers' posts for technical definitions. A Martin-style (in Gowers' terminology, "Ramsey") lift is a lift to a game of specifying some $y \in U$ coordinate by coordinate, where $U$ is the universe and is potentially larger than $2^n$, but now the winning condition is very simple: whether player I or II wins is decided based on the value of a single coordinate of $y$. As in Martin's proof, a lift must preserve winning strategies.
The hope that this may avoid the natural proofs barrier is based on the intuition that the property "has Martin style lift to a small universe" is probably not easy to compute. But at this point it's not clear if the parity function has a lift to a small universe. I worry that the appropriate analogy to Borel sets may be functions $f$ in AC0: finding a small lift for parity would put at least that worry to rest.
