Existence of infinite simple property-(T) LEF groups

Can an infinite simple discrete group have Kazhdan property (T) while being locally embeddable into finite groups? Such a group would also supply sofic and hyperlinear examples.

Why it matters and what counts as progress

Why it matters: The question combines rigidity with finite approximation in one simple group.

What counts as progress: One explicit witness with proofs of infinitude, simplicity, property (T) and local finite embeddability, or an obstruction to their coexistence.

How the problem developed

2001 · Open question [1][2]
Kenneth S. Brown Asked whether an infinite simple discrete group with property (T) can be hyperlinear; the later sofic version was recorded by Pestov.
13 Sept 2026 · Formalized result [3]
Palomar submission authors; Claude wrote the submission prose Gave a Lean proof of an infinite simple property-(T) group that is LEF, using periodic models of a binary Toeplitz shift; hence the witness is also sofic and hyperlinear.

AI contribution

An Infinite Simple Group with Property (T) That Is Sofic and Hyperlinear

Sauers

A group built as EL₃(LC(X,F₂)⋊ℤ), with X a binary Toeplitz subshift, is infinite and simple, has Kazhdan property (T), and is locally embeddable into finite groups. It is therefore sofic and hyperlinear. The Lean project compares two existential statements using this same witness.

AI involvementAI-led

ImportanceMajor

Technical verificationFormal (Lean 4/Mathlib kernel, Comparator and NanoDa)

Human understandingFew