The Aldous-Lyons conjecture asked whether every unimodular network (a random rooted graph satisfying a natural symmetry condition) can be approximated by finite graphs. The conjecture would mean that the space of unimodular networks is “tame” — every infinite random graph is a limit of finite ones, and the infinite doesn't introduce fundamentally new objects.
The conjecture is false, and the proof goes further: the problem of determining whether a given non-local game has a perfect strategy is undecidable. This undecidability, combined with a reduction from non-local games to network properties, implies the existence of unimodular networks that are non-sofic — they cannot be approximated by any sequence of finite graphs.
The proof adapts the compression technique from MIP* = RE, the landmark result that showed multi-prover interactive proofs with entanglement can verify any recursively enumerable language. The same machinery that proved the power of entangled provers also proves the existence of intrinsically infinite random graphs.
The structural point: the infinite is not always a limit of the finite. There exist well-defined, natural random graph structures that no finite sequence converges to. The distinction between “limits of finite objects” and “genuinely infinite objects” is not merely philosophical but mathematical — and the proof that the distinction exists is itself undecidable. You cannot algorithmically determine which side of the line a given network falls on.