The local-global conjecture for Apollonian circle packings is false

Problem statement

Notes: Unavailable.

Source: S. Haag, C. Kertzer, J. Rickards, and K. E. Stange, `The local-global conjecture for Apollonian circle packings is false`, Annals of Math, 200 (2) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2024-200-2-LocalGlobalApollonianCirclePackings.lean

Informal solution: Unavailable.

/--
Statement of Theorem 1.6:

The Apollonian circle packing `A` generated by `(−3, 5, 8, 8)` has no square curvatures.
-/
theorem declaration uses `sorry`theorem_1_6 : ∀ n, n ^ 2 ∉ curvatureSet ⟦⟨![-3, 5, 8, 8], byn:ℤ⊢ ![-3, 5, 8, 8] ∈ integralPrimitiveDescartesQuadruple decideAll goals completed! 🐙⟩⟧ := by⊢ ∀ (n : ℤ), n ^ 2 ∉ curvatureSet ⟦⟨![-3, 5, 8, 8], ⋯⟩⟧
  sorryAll goals completed! 🐙

/--
Statement of Theorem 1.3:

There exist infinitely many `A` for which the number of missing curvatures up to `N` is `Ω(√N)`.
-/
theorem declaration uses `sorry`theorem_1_3 : {A : PrimitiveApollonianCirclePacking |
    Real.sqrt =O[Filter.atTop] missingCurvatures A}.Infinite := by⊢ {A | Real.sqrt =O[Filter.atTop] missingCurvatures A}.Infinite
  sorryAll goals completed! 🐙