A new AI-generated proof of the existence of non-sofic groups relies on two central results of senior research fellow Gábor Kun and Kun–Thom.
OpenAI has announced ten new advances produced by an internal version of its forthcoming Astra model. The results concern long-standing problems in sphere packing, coding theory, group theory, operator algebras, circuit and quantum complexity, lattice problems, discrete geometry and extremal combinatorics. According to OpenAI, each argument has also been formalized in the Lean proof assistant.
One of the most striking results is the first construction of a non-sofic group. A group is called sofic if every finite fragment of its multiplication table can be approximated arbitrarily accurately by permutations of a finite set. The notion originated in the work of Mikhail Gromov in 1999, and Benjamin Weiss subsequently asked whether every countable group is sofic. The class contains, among others, all amenable and all
residually finite groups, and for more than twenty-five years no example outside it was known.
Earlier works by Gábor Elek, professor of Algebra Research Department and Endre Szabó, professor of Algebraic Geometry and Differential Topology Research Depatrment showed that sofic groups satisfy several properties conjectured to hold for broad classes of groups. In particular, they proved that sofic groups satisfy Kaplansky's Direct Finiteness Conjecture and Lück's Determinant Conjecture, and they also established that every sofic group is hyperlinear. Both researchers are to this date affiliated with the HUN-REN Alfréd Rényi Institute of Mathematics.
The new proof relies crucially on earlier results of Gábor Kun, a senior research fellow at Alfréd Rényi Institute of Mathematics, and on his joint work with Andreas Thom (who is a professor at Technische Universität Dresden). Kun proved that finite graphs approximating a group with Kazhdan’s property (T) can, after a negligible modification, be decomposed into uniformly expanding components. Kun and Thom then showed that sufficiently good approximations supported on a single expander impose strong finite-approximability properties on groups commuting with the property-(T) action.
The Astra-generated argument develops a new method for matching Kun’s separate expander components and extracting one expanding approximation to which the Kun–Thom theorem can be applied. A carefully chosen copy of Thompson’s group V then violates the required finite-approximability property, producing a contradiction and hence a non-sofic group. The manuscript explicitly identifies Kun’s decomposition theorem and the Kun–Thom result as the two principal inputs to this part of the proof.
Gabor Kun's publication can be reached HERE.