Commuting probabilities are closed

commProb_closed

Submitter: Thomas Browning.

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! 🐙

Solved by

• @LorenzoLuccioli with Aristotle (Harmonic) on Jul 15, 2026

• @GanjinZero with Seed Prover (ByteDance) on Jul 15, 2026