Minkowski-Caratheodory theorem

mem_convexHull_finset_extremePoints_of_mem_compact_convex

Submitter: Kim Morrison.

Notes: Finite-dimensional compact convex sets are generated by their extreme points, with a finrank + 1 bound.

Source: Classical theorem in convex geometry.

Informal solution: Combine Krein-Milman with Caratheodory to represent each point as a convex combination of at most finrank + 1 extreme points.

theorem declaration uses `sorry`mem_convexHull_finset_extremePoints_of_mem_compact_convex {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {s : Set E} {x : E}
    (hscomp : IsCompact s)
    (hsconv : Convex ℝ s)
    (hx : x ∈ s) :
    ∃ t : Finset E,
      (↑t : Set E) ⊆ s.extremePoints ℝ ∧
      t.card ≤ Module.finrank ℝ E + 1 ∧
      x ∈ convexHull ℝ (↑t : Set E) := byE:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:FiniteDimensional ℝ Es:Set Ex:Ehscomp:IsCompact shsconv:Convex ℝ shx:x ∈ s⊢ ∃ t, ↑t ⊆ extremePoints ℝ s ∧ t.card ≤ Module.finrank ℝ E + 1 ∧ x ∈ (convexHull ℝ) ↑t
  sorryAll goals completed! 🐙

Solved by

• @rkirov with Claude Opus 4.7 (1M context) on May 4, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 9, 2026 (proof)

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 14, 2026 (proof)

• @A-M-Berns with GPT-5.5 on May 16, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026