A common theme in mathematics is that limits of finite objects are well behaved. This allows one to prove many theorems about finitely approximable objects, while leaving the general case open --- examples for this are Gottschalk's conjecture, Kaplansky's direct finiteness conjecture, and many more. When the topology of the space is somewhat coarse, it becomes very hard to decide whether every object is approximable by finite ones, or whether there exist non-approximable objects. Some of the more famous problems in various fields of mathematics can be framed this way; this includes Connes' embedding problem (CEP) in functional analysis, the Aldous--Lyons conjecture in probability theory, the soficity problem of Gromov--Weiss in group theory, and more. In 2019, Ji--Natarajan--Vidick--Wright--Yuen resolved CEP in the negative, namely, they showed that there are non-approximable characters of the free group. The amazing thing about their result is that it is deduced from complexity theory, and specifically from undecidability in certain (quantum) interactive proof systems. Inspired by their work, we suggest a novel interactive proof system which is related to the Aldous--Lyons conjecture in the following way: If the Aldous--Lyons conjecture was true, then every language in this interactive proof system is decidable. A key concept we introduce for this purpose is that of a Subgroup Test, which is our analogue of a Non-local Game. By providing a reduction from the Halting Problem to this new proof system, we refute the Aldous-Lyons conjecture. In this first talk we introduce the main concepts, motivate the conjecture and give a high level description of the proof strategy. No special mathematical background will be assumed. This talk is based on a joint work with Lewis Bowen, Alex Lubotzky and Thomas Vidick.