In classical complexity theory, the PCP theorem arose directly from Babai, Fortnow, and Lund’s seminal result that multiprover interactive proof systems can decide NEXP. In the quantum case, the connection is less clear, but researchers have hoped that insights into the quantum PCP conjecture can arise from the study of succinct MIP* interactive proofs for QMA. In this talk, I will present the current state of knowledge regarding MIP* and QMA, explain a mistake in the proof of the “quantum games PCP conjecture” claimed by myself and Thomas Vidick in 2018, and discuss how these ideas may point the way towards interesting “baby versions” of the Hamiltonian quantum PCP conjecture. I will also discuss recent progress in setting of cryptographically sound argument systems, which a relaxed notion of interactive proof: here, recent work on “compiled” nonlocal games has led to succinct interactive arguments for QMA. Based on joint works with Chinmay Nirkhe, Tony Metger, and Tina Zhang.