{"id":"palomar/PALOMAR-2026-09-30-000032","url":"https://github.com/laurentbartholdi/theorem-a-fp-groups/tree/8970db6b7cc8ec2567dae486e48f34cf9226fe58","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000032-v1.json","repo":"https://github.com/laurentbartholdi/theorem-a-fp-groups","tags":["math.GR","msc:20J05","geometric-group-theory","finiteness-properties","lean-formalization"],"score":0,"title":"Embedding countable groups into groups of type FP_n","trust":"high","domain":"math.GR","source":"palomar","authors":["Laurent Bartholdi"],"reviews":0,"subject":"math.GR","summary":"A Lean formalization of Theorem A: every countable group embeds in a group of type FP_n over the integers for each finite n >= 2. The proof uses a 23-index, 15-triple Fano-plane construction to supply the finite input to geometric, homological, and relative Leary arguments. It does not assert the existence of one FP_infty overgroup.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Every countable group embeds in a group of type FP_n","identifier":"arXiv:2609.37562","relationship":"formalizes"}]}