A long-standing open problem in finite model theory is the question whether there exists a logic that captures polynomial time. Put differently, this question asks for a symmetry-invariant computation model which decides precisely the polynomial time computable properties of finite structures. Most logics that have been proposed were subsequently separated from polynomial time. One important candidate for which such a separation has not been achieved (in more than twenty years) is the logic Choiceless Polynomial Time (CPT). In this talk, I will introduce CPT along with techniques from finite model theory and group theory which can be used to reason about its limitations. Results obtained with these methods provide evidence that CPT may not be powerful enough to capture all of PTIME. I also suggest a concrete route towards separating CPT from PTIME via symmetric circuit lower bounds.
