OpenAI's Mathematical Breakthrough Builds on HUN-REN Rényi Researcher's Work

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 formalised 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 work by Gábor Elek, a professor in the Algebra Research Department, and Endre Szabó, a professor in the Algebraic Geometry and Differential Topology Research Department — both at the HUN-REN Alfréd Rényi Institute of Mathematics — 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 remain affiliated with the HUN-REN Alfréd Rényi Institute of Mathematics to this day.

The new proof relies crucially on earlier results by Gábor Kun, a senior research fellow at the HUN-REN Alfréd Rényi Institute of Mathematics, and on his joint work with Andreas Thom, 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.

Gábor Kun's publication is available here. The source of this article is available on HUN-REN Rényi"s website.