For a countable discrete group \(\Gamma \), the group von Neumann algebra \(L(\Gamma )\) is generated by the left regular representation of \(\Gamma \). When \(\Gamma \) has infinite conjugacy classes (ICC), meaning that every nonidentity conjugacy class is infinite, \(L(\Gamma )\) is a \(\mathrm {II}_1\) factor. The reconstruction question asks how much of \(\Gamma \) remains visible in that analytic completion.

Kazhdan's property (T) says that a unitary representation with almost invariant unit vectors has a nonzero invariant vector [ershov2010noncommutative, Section 3.1]. ICC makes the group von Neumann algebra a factor, while property (T) imposes representation-theoretic rigidity. These are the two hypotheses in the conjecture and in all three counterexample constructions below [zhou2026icc, Section 1, pp. 1–2].

Connes first proved that, for an ICC property-(T) group, \(\operatorname {Out}(L(\Gamma ))\) and the fundamental group \(\mathcal F(L(\Gamma ))\) are countable [zhou2026icc, Section 1, p. 1].

He subsequently proposed that such groups should be \(W^*\)-superrigid: for every countable group \(\Lambda \), an isomorphism \(L(\Lambda )\cong L(\Gamma )\) should force \(\Lambda \cong \Gamma \). Zhou's introduction states this original 1982 conjecture and distinguishes it from the later, narrower rigidity question for higher-rank lattices [zhou2026icc, Section 1, pp. 1–2].

The counterexamples considered here disprove the broad conjecture. They do not settle that higher-rank-lattice question.

The OpenAI and Zhou counterexamples were obtained independently and at nearly the same time. Zhou records that his preliminary manuscript predated the public OpenAI announcement, while acknowledging that the two projects were concurrent [zhou2026icc, Section 1, pp. 2–3].

OpenAI gives a countable family of pairwise nonisomorphic ICC property-(T) groups with isomorphic group factors [openai2026tenadvances, Chapter 4]. Zhou gives an explicit pair through a different action-changing construction [zhou2026icc, Theorem A and Section 3].

The later Anthropic proof gives another explicit pair by comparing a split extension with a nonsplit one [anthropic2026icc, Sections 3–5].

These are not three presentations of one proof. The algebraic datum hidden by the factor sits at a different level in each construction, and each factor argument removes it by a different measurable mechanism. The mathematical and formalization motivations for comparing them are stated next. The detailed OpenAI and Anthropic architectures appear in § [connes-000M] and § [connes-000N]; Sections 2–7 below follow Zhou's proof in its original order.

The motivation for this formalization experiment is threefold.

The Lean development turns the preceding motivations into one construction stage and four certificate lanes: factor equivalence, property (T), ICC, and group nonisomorphism. The final theorem assembles those four endpoints.

The diagram is a map of both the proof and the notes. Solid arrows are internal Lean developments. The dashed arrow is the sole substantive mathematical input left external: the Ershov–Jaikin-Zapirain–Kassabov property-(T) theorem for \(\mathrm {EL}_3(\mathbb F_2[t])\). Each lane uses a separate port at the construction and theorem nodes.

The mathematical weight is uneven:

• Construction. The characteristic-two calculation in Lemma [connes-000C], with its Lean realization in § [connes-000U], is concrete algebra and supplies every later carrier.
• Factor equivalence. Theorem [connes-0007], § [connes-000D], and § [connes-000E] carry heavy operator algebra: compact duals, Haar measure, Fourier transforms, von Neumann closures, and trace transport.
• Property (T). Definition [connes-0003], § [connes-000V], Theorem [connes-0004], § [connes-000Y], Lemma [connes-0005], and § [connes-000W] carry heavy harmonic and representation theory. Spectral measures and finite detectors are internal; EJZK enters at one boundary.
• ICC. Theorem [connes-0006] is the lightest lane conceptually, but its implementation in § [connes-000X] still needs exact orbit and finite-quotient displacement calculations.
• Nonisomorphism. Theorem [connes-0008] is the deepest internal algebraic chain. Characteristic kernels, quotient twists, semisimplicity, and a finite cocycle obstruction must survive an arbitrary isomorphism.

Most definitions and algebraic laws translate directly. Six interfaces require special design:

• the square-span certificate implemented in § [connes-000U];
• the Fourier-shear proof of factor equivalence: its unitary implementation in Theorem [connes-0007], its automatic projection-order transport in § [connes-001C], the four conjugation identities in § [connes-001D], and the measure and closure arguments in § [connes-000D] and § [connes-000E];
• the quantitative detector and qualitative property-(T) boundary in Definition [connes-0003], § [connes-000V], Theorem [connes-0004], and § [connes-000Y];
• the three-case ICC criterion in Theorem [connes-0006] and § [connes-000X];
• the quotient twist in § [connes-000H]; and
• the proposition-valued assembly in § [connes-0002].

The formalization lessons are discussed in § [connes-000A], § [connes-000F], § [connes-001C], § [connes-001D], and § [connes-000J].

The code has two layers. Reusable group theory, linear algebra, topology, measure theory, and operator algebra live in a foundation layer. Zhou-specific carriers and certificates live in construction and paper layers. This separation lets the paper-facing modules state small consumer interfaces while coordinate or finite calculations remain behind named certificates.

The public formalization plan and statement map give the complete module and declaration crosswalk.

Each lane exports the smallest object needed by its next consumer: a spatial witness, a qualitative property-(T) certificate, orbit and displacement data, or a twist-stable module obstruction.

Four corrections were mathematically decisive:

• replace identity-action scaffolds by Zhou's actions;
• make the ICC abstraction handle the finite \(\operatorname {Sp}_4(\mathbb F_2)\) factor;
• follow the quotient automorphism induced by a hypothetical group isomorphism; and
• tie the factor target to the Fourier shear and completed von Neumann closures.

The final interface remains proposition-valued. Its assembly and trust boundary are detailed in § [connes-0002] and Theorem [connes-0009]; the remaining EJZK work is scoped in § [connes-000B], § [connes-000G], and § [connes-000I]; the representation-universe boundary is recorded in § [connes-000L].

Section 1 separates the mathematical introduction, counterexample background, three motivations, and design. Sections 2–7 correspond respectively to Zhou's Sections 2–7; their headings record that correspondence without reusing Zhou's section number as the note title. Section 8 collects proof-engineering adaptations, Sections 9–10 compare the other two proof architectures, Section 11 scopes the remaining EJZK formalization, and Section 12 records the human–agent contribution and review workflow.

The formalization adapts selected public Lean proof blocks and organization patterns from a pinned openai/ten-proofs snapshot, but does not import that repository. The project records declaration-level adaptations in its public port map; the concrete Zhou carriers, corrected theorem boundaries, and final assembly are local to this development.