Existence of Non-Sofic Groups

Announced by OpenAI, 1 August 2026: an internal model ("Astra") produced a construction establishing the existence of non-sofic groups — the separation twenty-five years of human effort could not find. Part of a ten-result batch spanning operator algebras, coding theory and complexity, each accompanied by Lean-formalised certificates and expert review. As with all very recent claims, the community's digestion is ongoing; the announcement marks the boldest single batch of AI-originated group theory to date.

Context: every classical family is sofic — amenable, residually finite and initially subamenable (LEF) groups among them — so a non-sofic group must lie genuinely outside the approximable world, and no invariant was known to separate it. A construction is confirmed by exhibiting the group explicitly and proving no sequence of almost-actions approximates it; twenty-five years of failed attempts make the Lean-formalised certificate and independent expert review load-bearing parts of this claim rather than ornaments.