10 The Aldous–Lyons conjecture: subgroup tests
This chapter is the plan and the progress of Phase 6 of planning/aldous-lyons-track.md: the companion paper [ 37 ] of Bowen, Chapman, Lubotzky and Vidick, which with Chapter 9 refutes the Aldous–Lyons conjecture. Line numbers I:\(n\) refer to the LaTeX source of its arXiv version, which is the authority on the mathematics. Its argument has two halves. Main Theorem II (Theorem I:2126), finitary, associates with a tailored game a subgroup test whose sofic value is \(1\) when the game has a perfect ZPC strategy and bounded away from \(1\) when the game’s value is at most \(\frac12\). Main Theorem I (I:594) shows that under the conjecture the sofic value is approximable by a computable function. Together with a halting reduction to tailored games they contradict the undecidability of the halting problem.
Status. The definitions are formalized (MIPRE/SubgroupTestValue.lean, self-contained, and MIPRE/Tailored/Sofic/): subgroup tests and their sofic value, the Aldous–Lyons conjecture, and the associated test of a tailored game. Proved: the associated test is computable from the game (Lemma 10.5), and Main Theorem II with a halting reduction makes the sofic value not approximable (Theorem 10.19); and the perturbation half of Main Theorem II’s soundness (Proposition 10.10); Main Theorem II itself (Theorem 10.17); and so the sofic value is not approximable from a halting reduction to tailored games (Corollary 10.18). Main Theorem I (Theorems 10.23 and 10.28) is formalized too, so the Aldous–Lyons conjecture is false from a halting reduction to tailored games, and from a tailored answer reduction (Corollary 10.31). Paper II’s main theorem is proved (Theorem 9.21), so the conjecture is false (Corollary 10.32).
10.1 Subgroup tests and the conjecture
A subgroup test over the free group \(F\) on \(n\) generators is a finite list of weighted challenges, each a finite list \(K\) of words and a decision on the subsets of \(K\), here in disjunctive normal form over the literals “the \(i\)-th word of \(K\) lies in (or out of) the subgroup”. A finite action \(\sigma \) of \(F\) on a set of size \(N \geq 1\) gives the finitely described IRS \(\Phi (\sigma )\), the stabilizer of a uniform point; its value against the test is the probability that the stabilizer passes a challenge drawn with probability proportional to its weight. The sofic value of the test is the supremum of the values of finite actions.
The sofic value is approximable when a computable function \(f\) of a test \(T\) and \(k \in \mathbb {N}\) satisfies \(|\mathrm{val}_{\mathrm{sof}}(T) - f(T, k)/(k+1)| \leq 1/(k+1)\) for all \(T\) and \(k\).
The space \(\mathrm{Sub}(F)\) of subgroups of the free group on \(s\) generators is a closed subspace of \(\{ 0,1\} ^F\) with the product topology. An invariant random subgroup is a Borel probability measure on it invariant under conjugation; the finitely described ones are the measures \(\Phi (\sigma )\) of finite actions. The Aldous–Lyons conjecture asserts that for every \(s\) the finitely described IRSs are weak-\(*\) dense in the IRSs.
10.2 The test associated with a tailored game
The test associated with a tailored game has a generator \(J\) and one generator for each variable of each vertex, and one challenge per question pair, with the pair’s weight. A subgroup \(H\) passes the challenge at \((x, y)\) when: \(J \notin H\), \(J^2 \in H\) and \(J\) commutes in \(H\) with the variables at \(x\) and \(y\) (Check 1); the variables are involutions and those at a vertex commute (Check 2); each readable variable \(X\) has \(X \in H\) or \(J X \in H\), which reads off a value \(r\) of the readable variables (Check 3); and the word \(J^{c_J} \prod X^{c}\) of every constraint \(c \in L_{xy}(r)\) lies in \(H\) (Check 4). It is written as one clause per readable value \(r\), and the constraint words are deduplicated, which bounds their number by \(2^{2\Lambda + 1} + 1\). An action passes Checks 1–3 everywhere when \(J\) is a fixed-point-free involution commuting with the variables, these are involutions commuting at each vertex, and each readable variable acts at every point as the identity or as \(J\).
The map from a tailored game description to the description of its associated test is primitive recursive.
Each construction is a composition of list operations. Three are rewritten first: the readable values as an iterate, deduplication as a fold, and the enumeration of the fixed literals by a range.
The normalized Hamming distance of two permutations of a finite set, the fraction of points where they differ, satisfies the triangle inequality, is subadditive on products, and is invariant under inversion.
Counting points.
A permutation \(\pi \) is within \(d(\pi ^2, 1)\) of an involution; an involution of an even set almost without fixed points is close to one without, given a fixed-point-free involution commuting with it; and a family of involutions at a vertex, together with \(J\), can be made into commuting involutions commuting with \(J\), the readable ones acting as the identity or as \(J\), by changing them on at most \(2^{\ell + 1}\) times the points at which some relation fails.
The first two as in the paper. The third replaces Claim I:2600 and Glebsky–Rivera (Claim I:2631): restrict the variables to the set of points from which every ordered product of them reaches only points where all relations hold, invariant under the variables and \(J\), and let them act as the identity elsewhere.
For two actions of the generators on the same finite set, \(|\mathrm{val}(T, \sigma ) - \mathrm{val}(T, \sigma ')| \leq \sum _k S_T(k)\, d(\sigma _k, \sigma '_k)\), where the significance \(S_T(k)\) is the expected number of occurrences of the generator \(k\) in the words of a challenge.
A word moves a point differently under the two actions only if one of its letters does at an intermediate point; letters and their inverses cost the same.
In the associated test every generator has significance at most a bound \(S(\Lambda )\) of order \(\Lambda 4^{\Lambda }\), and the variables at a vertex \(x\) at most \(S(\Lambda )\) times the weight of the question pairs containing \(x\).
The words of the challenge at \((x, y)\) use only \(J\) and the variables at \(x\) and \(y\); their number and lengths are bounded, the constraint words by deduplication.
If an action has value at least \(1 - \varepsilon \) against the associated test of a tailored game with answer length \(\Lambda \), then an action passing Checks 1–3 everywhere has value at least \(1 - 300\, (\Lambda + 1)^4\, 2^{4(\Lambda + 1)}\, \varepsilon \).
Double the action first, so that the set is even and carries a fixed-point-free involution commuting with every generator. Make \(J\) a fixed-point-free involution, then repair the variables vertex by vertex (Lemma 10.7), bounding the points changed at a vertex by its losing probability, and conclude by robustness and significance.
A permutation strategy for a tailored game (signed permutation observables, involutions commuting at each vertex, diagonal at the readable variables, the identity beyond each vertex’s length) need not commute along edges; its Fourier-transform measurements still form a synchronous strategy, with the same value, so its value is at most the game’s synchronous value.
For such a strategy, the sum over the answer pairs whose readable parts lie in a set \(R\) of \(\mathrm{Tr}(P_a\, X\, Q_b)\) is the sum of the diagonal entries \(X_{jj}\) over the basis points \(j\) whose readable signs lie in \(R\). For a constraint \(c\) with matrix \(M_c = (-1)^{c_J} U^{\alpha } V^{\beta }\), the probability that the readable parts are \(r\) and \(c\) is violated is \(\frac1m \sum _{j \in R_r} \frac{1 - (M_c)_{jj}}{2}\).
A basis point lies in the support of \(P_a\) only if its readable signs are those of \(a\), and the projections sum to the identity; the observable of a constraint is \((-1)^{\langle c, (a, b, 1) \rangle }\) on the range of \(P_a \otimes Q_b\).
For an action passing Checks 1–3 everywhere, a point passes the challenge at \((x, y)\) exactly when the constraint words of the entries whose readable part is the point’s readable value fix it; and there are at most \(2^{\ell (x) + \ell (y) + 1} + 1\) constraint words.
The fixed literals and the readable literals of the point’s own clause hold, and those of every other clause fail since \(J\) moves every point.
Let an action pass Checks 1–3 everywhere. Choosing one point of each \(J\)-orbit, every permutation commuting with \(J\) induces a signed permutation of the representatives, multiplicatively, sending \(J\) to \(-1\), with sign \(+\) at \(r\) exactly when it fixes \(r\). The variables induce a Z-aligned signed-permutation strategy, in which the matrix of a constraint is the signed permutation induced by its word.
A permutation commuting with \(J\) permutes the \(J\)-orbits; the readable variables act as the identity or as \(J\), hence diagonally.
An action passing Checks 1–3 everywhere with value \(1 - \varepsilon \) against the associated test gives the game a synchronous value at least \(1 - 2 \cdot 2^{2(\Lambda + 1)} \varepsilon \).
By the trace identity, the game’s rejection mass at \((x, y)\) is at most the sum over the distinct constraint words of the fraction of representatives they do not fix, hence at most the number of constraint words, twice, times the test’s failure probability at \((x, y)\); there are at most \(2^{2(\Lambda + 1)}\) of them. This replaces the paper’s Fourier bases and orbit decompositions.
A perfect ZPC strategy of a tailored game lifts to an action of value \(1\) against the associated test: on twice the points, \(J\) swapping the copies and each variable acting by its signed permutation.
Checks 1–3 hold at every point. By the trace identity at value \(1\), every constraint word of a pair of positive weight fixes the points of its readable value, so every point passes every challenge of positive weight. Commutation along edges is not used.
Let \(G\) be a tailored game with answer length \(\Lambda \). If \(G\) has a perfect ZPC strategy, its associated test has sofic value \(1\). If its associated test has sofic value at least \(1 - \varepsilon \), then \(G\) has synchronous value at least \(1 - 600 (\Lambda +1)^4 2^{6(\Lambda +1)} \varepsilon \). So the clauses of Theorem 10.19 hold with the primitive recursive gap \(K(\Lambda ) = 600 (\Lambda +1)^4 2^{6(\Lambda +1)}\).
A halting reduction to tailored games makes the sofic value of subgroup tests not approximable; in particular a tailored answer reduction at input level \(5\) does.
10.3 The sofic value is not approximable
Given a computable halting reduction to tailored games, and the two clauses of Main Theorem II with a primitive recursive gap function \(K(\Lambda )\), the sofic value is not approximable.
Approximate the sofic value of the associated test of the game of a machine at \(k = 4K(\Lambda )\). A halting machine gives sofic value \(1\), so the approximation is at least \(k/(k+1)\); a non-halting one gives sofic value at most \(1 - 1/(2K)\), and the approximation is less than \(k/(k+1)\). The comparison is computable, and decides the halting problem.
10.4 The measure side: Main Theorem I
The value of a test \(T\) against a probability measure \(\mu \) on \(\mathrm{Sub}(F)\) is the weighted average over challenges of the measure of the set of subgroups passing the challenge. The ergodic value \(\mathrm{val}_{\mathrm{erg}}(T)\) is its supremum over the invariant random subgroups. A finite action \(\sigma \) gives the measure \(\Phi (\sigma )\), the stabilizer of a uniform point.
The value against a measure is weak-\(*\) continuous, and the value against \(\Phi (\sigma )\) is the value of \(\sigma \). Finitely described IRSs are IRSs.
Each passing set is clopen in the product topology, so its measure is continuous in \(\mu \); the value is a finite weighted sum of these.
For every test, \(\mathrm{val}_{\mathrm{sof}}(T) \leq \mathrm{val}_{\mathrm{erg}}(T)\), and if the Aldous–Lyons conjecture holds they are equal.
The finitely described IRSs are IRSs; under the conjecture every IRS is a weak-\(*\) limit of finitely described ones, and the value is continuous.
There is a primitive recursive \(\alpha (T, t)\) such that \(\alpha (T,t)/2^t\) is non-decreasing in \(t\), at most \(\mathrm{val}_{\mathrm{sof}}(T)\), and converges to it.
Enumerate the finite actions by codes; \(\alpha (T, t)/2^t\) is the largest value of the first \(t\) codes’ actions, rounded down to a multiple of \(2^{-t}\).
Index the indicator of a subgroup by words rather than group elements. A probability measure on word indicators carried by the indicators that respect free reduction and the subgroup axioms, and invariant under conjugation by each letter, is the image of an IRS with the same value against every test.
The good indicators are the complement of a countable union of clopen sets, and on them evaluation at a reduced word is a subgroup indicator; push forward and check invariance on generators.
At stage \(t\) take the words of length at most \(t+2\) in the first \(n+t\) letters, and the grid points of weight \(M = P \cdot 2^t\) on its \(P\) patterns. A grid point is feasible when every pattern of positive weight is locally closed (contains the empty word, closed under cancelling a pair, deleting a letter beyond the \(n\) generators, and \(u, v \mapsto u v^{-1}\) within the stage) and conjugation by each generator moves it by at most \(4P\) in \(\ell ^1\). The upper value at stage \(t\) is the best value of a feasible point, plus \(2/2^t\), rounded up to a multiple of \(2^{-t}\). This replaces the paper’s pseudo IRS polytope and its linear program by an exhaustive search over a grid, with the invariance relaxed to absorb rounding.
For every stage \(t\), \(\mathrm{val}_{\mathrm{erg}}(T) \leq \mathrm{upper}(T, t)/2^t\).
Round the restriction of an IRS to the stage’s words to the grid: it is feasible, and its value is within \(2/2^t\) of the IRS’s.
\(\mathrm{upper}(T, t)/2^t \to \mathrm{val}_{\mathrm{erg}}(T)\).
Lift the optimal feasible point of each stage to a measure on word indicators. The probability measures on word indicators form a compact space, so a subsequence converges; the limit is carried by the good indicators and is invariant, because the cylinder sets are a generating \(\pi \)-system and the stage’s conditions hold on ever more of them. By Lemma 10.24 it is an IRS, and the value is continuous.
There is a primitive recursive \(\beta (T, t)\) such that \(\beta (T,t)/2^t\) is non-increasing in \(t\), at least \(\mathrm{val}_{\mathrm{erg}}(T)\), and converges to it.
The running minimum of the upper values, which is primitive recursive because the stage search is.
If the Aldous–Lyons conjecture holds, the sofic value is approximable.
Under the conjecture both sequences converge to the same value from either side; run them until their gap is at most \(1/(k+1)\), which happens, and output a point between them.
A halting reduction to tailored games refutes the Aldous–Lyons conjecture.
A tailored answer reduction at input level \(5\) refutes the Aldous–Lyons conjecture.
The sofic value of subgroup tests is not approximable, and the Aldous–Lyons conjecture is false.
- 1
Z. Ji, A. Natarajan, T. Vidick, J. Wright, H. Yuen. \(\mathrm{MIP}^* = \mathrm{RE}\). arXiv:2001.04383, 2020 (revised 2022).
- 2
Z. Ji, A. Natarajan, T. Vidick, J. Wright, H. Yuen. Quantum soundness of the classical low individual degree test. arXiv:2009.12982, 2020.
- 3
Z. Ji, A. Natarajan, T. Vidick, J. Wright, H. Yuen. Quantum soundness of testing tensor codes. Discrete Analysis, 2024:6. arXiv:2111.08131.
- 4
A. Coladangelo, J. Stark. Robust self-testing for linear constraint system games. arXiv:1709.09267, 2017.
- 5
A. Natarajan, T. Vidick. A quantum linearity test for robustly verifying entanglement. STOC 2017. arXiv:1610.03574.
- 6
A. Natarajan, J. Wright. \(\mathrm{NEEXP} \subseteq \mathrm{MIP}^*\). In Proc. 60th FOCS, 2019. arXiv:1904.05870.
- 7
W. T. Gowers, O. Hatami. Inverse and stability theorems for approximate representations of finite groups. Sbornik: Mathematics, 208(12):1784–1817, 2017. arXiv:1510.04085.
- 8
M. de la Salle. Orthogonalization of positive operator valued measures. arXiv:2103.14126, 2021.
- 9
T. Vidick. Almost synchronous quantum correlations. Journal of Mathematical Physics, 63(2):022201, 2022. arXiv:2103.02468.
- 10
M. Bavarian, T. Vidick, H. Yuen. Hardness amplification for entangled games via anchoring. In Proc. 49th STOC, 2017. arXiv:1509.07466.
- 11
A. Marks, S. S. Nezhadi, H. Yuen. The recursive compression method for proving undecidability results. Manuscript.
- 12
J. Lin. Tracially embeddable strategies: lifting MIP\(^*\) tricks to MIP\(^{\mathrm{co}}\). arXiv:2304.01940, 2023.
- 13
J. Lin. \(\mathrm{MIP}^{\mathrm{co}} = \mathrm{coRE}\). In Proc. 58th STOC, 2026. arXiv:2510.07162.
- 14
X. Wu, J.-D. Bancal, M. McKague, V. Scarani. Device-independent parallel self-testing of two singlets. Physical Review A, 93:062121, 2016. arXiv:1512.02074.
- 15
J. Fitzsimons, Z. Ji, T. Vidick, H. Yuen. Quantum proof systems for iterated exponential time, and beyond. In Proc. 51st STOC, 2019. arXiv:1805.12166.
- 16
W. Slofstra. The set of quantum correlations is not closed. Forum of Mathematics, Pi, 7:E1, 2019. arXiv:1703.08618.
- 17
M. Junge, M. Navascués, C. Palazuelos, D. Pérez-García, V. Scholz, R. Werner. Connes’ embedding problem and Tsirelson’s problem. Journal of Mathematical Physics, 52(1):012102, 2011.
- 18
T. Fritz. Tsirelson’s problem and Kirchberg’s conjecture. Reviews in Mathematical Physics, 24(05):1250012, 2012.
- 19
N. Ozawa. About the Connes embedding conjecture: algebraic approaches. Japanese Journal of Mathematics, 8(1):147–183, 2013.
- 20
S.-J. Kim, V. Paulsen, C. Schafhauser. A synchronous game for binary constraint systems. Journal of Mathematical Physics, 59(3):032201, 2018.
- 21
V. Paulsen, S. Severini, D. Stahlke, I. Todorov, A. Winter. Estimating quantum chromatic numbers. Journal of Functional Analysis, 270(6):2188–2222, 2016.
- 22
C. Papadimitriou, M. Yannakakis. A note on succinct representations of graphs. Information and Control, 71(3):181–185, 1986.
- 23
S. Cook. The complexity of theorem-proving procedures. In Proc. 3rd STOC, 1971.
- 24
V. Shoup. New algorithms for finding irreducible polynomials over finite fields. Mathematics of Computation, 54(189):435–447, 1990.
- 25
H. W. Lenstra, Jr. Finding isomorphisms between finite fields. Mathematics of Computation, 56(193):329–347, 1991.
- 26
J. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. Journal of the ACM, 27(4):701–717, 1980.
- 27
R. Zippel. Probabilistic algorithms for sparse polynomials. In Symbolic and Algebraic Computation, pages 216–226, 1979.
- 28
J. W. Helton, S. A. McCullough. A Positivstellensatz for non-commutative polynomials. Transactions of the American Mathematical Society, 356(9):3721–3737, 2004.
- 29
M. Navascués, S. Pironio, A. Acín. A convergent hierarchy of semidefinite programs characterizing the set of quantum correlations. New Journal of Physics, 10(7):073013, 2008.
- 30
B. Durand, A. Romashchenko, A. Shen. Fixed-point tile sets and their applications. Journal of Computer and System Sciences, 78(3):731–764, 2012.
- 31
OpenAI. Ten advances in mathematics and theoretical computer science. Chapter 6: Exponential parallel repetition for all two-player entangled games. 2026. https://cdn.openai.com/pdf/ten-proofs-oai.pdf; Lean formalization at https://github.com/openai/ten-proofs.
- 32
T. Vidick. Uniform direct parallel repetition for two-player commuting-operator strategies. Manuscript with Lean formalization, 2026. https://github.com/vidick/commuting-repetition.
- 33
Adversarial verification campaign of the mipre-proof manuscript. Repository vidick/mipre-proof at commit 4768735, 2026; report on this blueprint of 11 September 2026, with its ledger and claim-tests. The findings acted on, and those deferred, are recorded in planning/next-steps.md. Claims it makes about sources not vendored here are marked as unverified where they are used below.
- 34
Companion paper and proof ledger. Repository vidick/MIPRE-proof at commit a459dee4413a256107fc2d227bab298eba04051c, consulted September 2026. Current source contracts and reviewed corrections; the correspondence and remaining formalization adapters are recorded in planning/paper-correspondence.md. Ledger review is distinct from a Lean proof.
- 35
S. Basu, R. Pollack and M.-F. Roy. Algorithms in Real Algebraic Geometry, 2nd edition. Algorithms and Computation in Mathematics 10, Springer, 2006.
- 36
L. Bowen, M. Chapman, T. Vidick. The Aldous–Lyons conjecture II: undecidability. arXiv:2501.00173, 2025.
- 37
L. Bowen, M. Chapman, A. Lubotzky, T. Vidick. The Aldous–Lyons conjecture I: subgroup tests. arXiv:2408.00110, 2024.