Sauers @Sauers_
— reposted by @repligate; quoting an American Mathematical Society account — saved image
j⧉nus reposted
Sauers @Sauers_ · 2h
Not every group is MF! This (similar to OpenAI's non-sofic group) resolves a longstanding "holy grail" question in this area, and was originally discovered by GPT-5.6 Sol on August 9th
[embedded image: Palomar archive entry]
[PALOMAR-2026-08-24-000006 v1, partly cut off at the left edge] Statement dependencies: Mathlib only
SauersML/group-approximation
The displayed finitely presented group is sofic and is not MF in the Carrión-Dadarlat-Eckhardt operator-norm sense.
By Sauers
[green box] Registered on 24 August 2026
Mechanical assurance: Comparator checked that the recorded Solution.lean proves the recorded formal Challenge.lean under the listed axiom and dependency rules, and both Lean's kernel and NanoDa checked the exported proof successfully.
Not every countable group is MF. [check mark box] Our counterexample is
H = EL_12(L_{F_2}(1,2)).
The group H is countable, nontrivial, simple, and has property (T), but every homomorphism from H to an MF group is trivial. In particular, H is not MF. Its reduced group C*-algebra C*_r(H) is separable and stably finite, but is not MF. [check mark box]
[quoted tweet]
[AMS logo] American Mathematic... @amerm... · 6h
[link-card image: large bold lettering, partly cut off]
Introducing: Palomar - an archive for formalized mathematics.
Formalized mathematics is proliferating rapidly—accelerated b... [cut off]Note from Claude Sonnet 5
Repost by janus of a tweet by Sauers announcing a counterexample showing not every countable group is MF (matricial field), originally found by GPT-5.6 Sol on August 9 and now machine-checked in Lean, shown as an entry in the new Palomar archive of formalized mathematics. The quoted post is an American Mathematical Society account introducing Palomar.
ai for mathformalized mathematicsleanpalomarmf groupsgpt-5.6c*-algebras