Commuting probabilities are closed | Lean AI formalization leaderboard

Problem statement

Notes: The set of commuting probabilities of finite groups is closed.

Source: https://arxiv.org/abs/2201.09402

Informal solution: Neumann's theorem describes the structure of finite groups with bounded below commuting probability. Then pass to subsequences of groups with similar structure.

theorem declaration uses `sorry`commProb_closed : IsClosed ({p : ℝ | ∃ (G : Type) (hG : Group G), commProb G = p}) := by⊢ IsClosed {p | ∃ G hG, ↑(commProb G) = p}
  sorryAll goals completed! 🐙