On property (T) for Aut(F_n) and SL_n(Z) | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: M. Kaluba, D. Kielak, and P. W. Nowak, `On property (T) for Aut(F_n) and SL_n(Z)`, Annals of Math, 193 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-193-2-OnPropertyT.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1 (n : ℕ) (hn : n ≥ 6) : OnPropertyT.PropertyT (MulAut (FreeGroup (Fin n))) := byn:ℕhn:n ≥ 6⊢ PropertyT (MulAut (FreeGroup (Fin n)))
  sorryAll goals completed! 🐙