/-- **Higman's infinite simple group** (G. Higman 1951/1974). There
exists an infinite finitely presented simple group. -/
theorem higman_infinite_simple :
    ∃ (n : ℕ) (rels : Set (FreeGroup (Fin n))),
      rels.Finite ∧ IsSimpleGroup (PresentedGroup rels) ∧
        Infinite (PresentedGroup rels) := by
  sorry

/-- **Fáry–Milnor theorem** (Fáry 1949 / Milnor 1950). A smooth knot
with total curvature at most `4π` is unknotted. -/
theorem fary_milnor_total_curvature
    {r : ℝ → Space} (_hknot : IsSmoothKnot r)
    (_hK : totalCurvature r ≤ 4 * Real.pi) :
    IsUnknotted r := by
  sorry

/-- **Novikov's theorem** (P.S. Novikov 1955; independently W.W. Boone
1958). There exists a finite presentation with undecidable word
problem. -/
theorem novikov_unsolvable :
    ∃ (n : ℕ) (rels : Set (FreeGroup (Fin n))),
      rels.Finite ∧ ¬ WordProblemSolvable (PresentedGroup.mk rels) := by
  sorry

/-- **Existence of a chiral oriented smooth knot.**

There exists an oriented smooth knot in `ℝ³` that is not ambient-isotopic
to its mirror image (the reflection of the image through the `xy`-plane).

*Suggestion.* The right-handed trefoil is chiral. Parametrize it for
instance as

  `t ↦ (sin t + 2 sin (2 t), cos t − 2 cos (2 t), −sin (3 t))`.

Here chirality is understood in the orientation-sensitive sense induced by
the benchmark's notion of isotopy. Proving chirality therefore requires an
ambient-isotopy invariant that takes *different* values on a knot and its
mirror image. The figure-eight knot *is* isotopic to its mirror in the usual
unoriented sense, so the invariant must be sensitive to chirality — in
particular, the knot determinant and the Alexander polynomial alone do *not*
suffice (both are mirror-symmetric).

Standard chirality-detecting invariants:

* The **knot signature** `σ(K) ∈ ℤ`, computed from a Seifert matrix
  `V` as the signature of `V + Vᵀ`. Mirroring negates the signature, so
  any knot with `σ(K) ≠ 0` is chiral. The right-handed trefoil has
  `σ = −2`.
* The **Jones polynomial** `V_K(t) ∈ ℤ[t^{1/2}, t^{-1/2}]`. Mirroring
  sends `V_K(t)` to `V_K(t⁻¹)`, so any knot whose Jones polynomial is not
  symmetric under `t ↔ t⁻¹` is chiral. The right-handed trefoil has
  `V_K(t) = −t^{−4} + t^{−3} + t^{−1}`.

See <https://en.wikipedia.org/wiki/Chirality_(mathematics)> and
<https://en.wikipedia.org/wiki/Trefoil_knot>. -/
theorem exists_chiral_knot : ∃ K : Knot, K.Chiral := by
  sorry

/-- **Dehn–Sommerville equations.** The h-vector of a finite simplicial sphere
is symmetric: `h_j = h_{d-j}`. -/
theorem dehn_sommerville
    {d j : ℕ} (X : FiniteSimplicialSphere d) (hj : j ≤ d) :
    hVector X j = hVector X (d - j) := by
  sorry

/-- **Fatou–Julia dichotomy.** For the quadratic family, `c ∈ M` implies
the filled Julia set `K_c` is connected; `c ∉ M` implies `K_c` is
homeomorphic to the Cantor space `ℕ → Bool`. -/
theorem julia_cantor_dichotomy (c : ℂ) :
    (c ∈ Mandelbrot → IsConnected (FilledJulia c)) ∧
    (c ∉ Mandelbrot → Nonempty ((FilledJulia c) ≃ₜ (ℕ → Bool))) := by
  sorry

/-- **Gleason's theorem**, finite-dimensional version. For `dim H ≥ 3`, every frame
function on the projection lattice of `H` is given by `P ↦ re Tr(ρ P)` for the unique
density operator `ρ` (positive, `re Tr ρ = 1`). -/
theorem gleason_theorem_finite
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [FiniteDimensional ℂ H]
    (hdim : 3 ≤ Module.finrank ℂ H)
    (f : FrameFunction H) :
    ∃! ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      reTr ρ = 1 ∧
      ∀ P : H →L[ℂ] H, IsOrthProj P → f.μ P = reTr (ρ * P) := by
  sorry

/-- **KAM theorem (persistence of an invariant curve).** For real-analytic,
`1`-periodic, non-constant, mean-zero `f` and Diophantine `α`, for all small
`|c|` the twist-map functional equation
`q(t+α) − 2q(t) + q(t−α) = c·f(q(t))` has a smooth strictly increasing solution
`q` with `q − id` periodic — the `c = 0` curve `q₀(t) = t` persists as a smooth
invariant curve of rotation number `α`. -/
theorem kam_invariant_curve
    (α : ℝ) (_hα : IsDiophantine α)
    (f : ℝ → ℝ)
    (_hf_analytic : AnalyticOnNhd ℝ f Set.univ)
    (_hf_per : Function.Periodic f 1)
    (_hf_nonconst : ¬ ∃ k : ℝ, ∀ x, f x = k)
    (_hf_mean : ∫ x in (0 : ℝ)..1, f x = 0) :
    ∃ c₀ : ℝ, 0 < c₀ ∧ ∀ c : ℝ, |c| < c₀ →
      ∃ q : ℝ → ℝ,
        ContDiff ℝ ∞ q ∧ StrictMono q ∧
        Function.Periodic (fun t => q t - t) 1 ∧
        ∀ t : ℝ, q (t + α) - 2 * q t + q (t - α) = c * f (q t) := by
  sorry

/-- **There are exactly 17 wallpaper groups** (Pólya–Niggli 1924). -/
theorem there_are_17_wallpaper_groups :
    crystallographicCount 2 = 17 := by
  sorry

/-- **Margulis–Ruelle inequality (1968/1978).** `h_μ(T) ≤ λ₁⁺ + λ₂⁺`. -/
theorem margulis_ruelle
    (T T_inv : EucPlane → EucPlane)
    (hT_smooth : ContDiff ℝ 2 T)
    (hT_inv_smooth : ContDiff ℝ 2 T_inv)
    (hT_left : Function.LeftInverse T_inv T)
    (hT_right : Function.RightInverse T_inv T)
    (K : Set EucPlane)
    (hK_compact : IsCompact K)
    (hK_inv : T '' K = K)
    (μ : Measure EucPlane) [IsProbabilityMeasure μ]
    (hμ_supp : μ Kᶜ = 0)
    (hμ_pres : MeasurePreserving T μ μ)
    (hμ_erg : Ergodic T μ) :
    kolmogorovSinaiEntropy μ T
      ≤ max 0 (∫ x, lyapunovUpperAt T x ∂μ)
          + max 0 (∫ x, lyapunovLowerAt T x ∂μ) := by
  sorry

/-- **Mergelyan's theorem.** For a compact `K ⊆ ℂ` with connected
complement and `f : ℂ → ℂ` continuous on `K` and analytic on the
interior of `K`, every `ε > 0` admits a complex polynomial `p` with
`‖f z − p(z)‖ < ε` on `K`. -/
theorem mergelyan (K : Set ℂ) (_hK : IsCompact K) (_hKc : IsConnected (Kᶜ))
    (f : ℂ → ℂ) (_hfc : ContinuousOn f K) (_hfh : AnalyticOnNhd ℂ f (interior K))
    (ε : ℝ) (_hε : 0 < ε) :
    ∃ p : ℂ[X], ∀ z ∈ K, ‖f z - p.eval z‖ < ε := by
  sorry