Absolute profinite rigidity and hyperbolic geometry | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: M. R. Bridson, D. B. McReynolds, A. W. Reid, and R. Spitler, `Absolute profinite rigidity and hyperbolic geometry`, Annals of Math, 192 (3) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-192-3-AbsoluteProfiniteRigidity.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_7_1 : AbsoluteProfiniteRigidity.ProfinitelyRigid (AbsoluteProfiniteRigidity.BianchiGroup 3) := by⊢ ProfinitelyRigid (BianchiGroup 3)
  sorryAll goals completed! 🐙