Проверка Lean-ом результата о вложении любой счетной группы в FP_n. 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. (помимо прочего, эта конструкция дает решения старых проблем из списка Бествины, проблема 8.7)