The complexity of simple stochastic games (SSGs) has been open since they were defined by Condon in 1992. Such a game is played by two players, Min and Max, on a graph consisting of max nodes, min nodes, and average nodes. The goal of Max is to reach the 1-sink, while the goal of Min is to avoid the 1-sink. When on a max (min) node, Max (Min) chooses the outedge, and when on an average node, they take each edge with equal probability. The complexity problem is to determine, given a graph, whether or not Max has a strategy that is guaranteed to reach the 1-sink with probability at least 1/2. Despite intensive effort, the complexity of this problem is still unresolved. In this paper, we establish a new connection between the complexity of SSGs and the complexity of an important problem in proof complexity--the proof search problem for low depth Frege systems. We prove that if depth-3 Frege systems are weakly automatizable, then SSGs are in P.Moreover we identify a natural combinatorial principle, which is a version of the well-known Graph Ordering Principle (GOP), that we call the integer valued GOP (IGOP). This principle states that for any graph $G$ with nonnegative integer weights associated with each node, there exists a locally maximal vertex (a vertex whose weight is at least as large as its neighbors). We prove that if depth-2 Frege plus IGOP is weakly automatizable, then SSG is in P.This is joint work with Lei Huang.