We survey results on the formalization and independence of mathematical statements related to major open problems in computational complexity theory. Our primary focus is on recent findings concerning the (un)provability of complexity bounds within theories of bounded arithmetic. This includes the techniques employed and related open problems, such as the ... more >>>

In a 3-XOR game \mathcal{G}, the verifier samples a challenge (x,y,z)\sim \mu where \mu is a probability distribution over \Sigma\times\Gamma\times\Phi, and a map t\colon \Sigma\times\Gamma\times\Phi\to\mathcal{A} for a finite Abelian group \mathcal{A} defining a constraint. The verifier sends the questions x, y and z to the players Alice, Bob and Charlie ... more >>>

The notion of closure of a set of linear forms, first introduced by Efremenko, Garlik, and Itsykson [EGI-STOC-24], has proven instrumental in proving lower bounds on the sizes of regular and bounded-depth Res(\oplus) refutations [EGI-STOC-24, AI-STOC-25]. In this work, we present amortized closure, an enhancement that retains the properties of ... more >>>