{"id":"palomar/PALOMAR-2026-09-13-000002","url":"https://github.com/SauersML/group-approximation/tree/a593f2e6166dc754348d76e808b86f05c3b21df9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-13-000002-v2.json","repo":"https://github.com/SauersML/group-approximation","tags":["math.GR","math.OA","math.DS","msc:20E32","msc:20F65","msc:22D55","msc:37B10","msc:20F69","group-theory","property-t"],"score":0,"title":"An Infinite Simple Group with Property (T) That Is Sofic and Hyperlinear","trust":"high","domain":"math.GR","source":"palomar","authors":["Sauers"],"reviews":0,"subject":"math.GR","summary":"Brown asks in 2001 (arXiv:math/0111286, Question 11.7) whether an infinite simple discrete group with Kazhdan's property (T) can embed in the unitary group of an R^ω-embeddable McDuff factor, which for such a group is hyperlinearity; Ozawa asks it in 2003 in that language, in About the QWEP conjecture (arXiv:math/0306067); and Pestov prints it, with the sofic form added, as Open question 9.1 of Hyperlinear and sofic groups: a brief guide (arXiv:0804.3968): can an infinite simple group with Kazhdan's property (T) be hyperlinear, or sofic? This project proves, in Lean 4 over Mathlib, that the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-13","reactions":{},"formalized":true}