Three random points on a circumference containing the origin

Stream: mathlib4

[Jeremy Tan]

Here should be a stiff challenge. Formalise any solution to this well-known little puzzle:
https://math.stackexchange.com/questions/268635

import Mathlib.Analysis.SpecialFunctions.Complex.Circle
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

open MeasureTheory

/-- A predicate expressing that the triangle formed by the three given points on the unit circle
contain the origin. -/
def ContainsOrigin (pts : Fin 3 → UnitAddCircle) : Prop :=
  ∃ w : Fin 3 → ℝ, 0 ≤ w ∧ ∑ i, w i = 1 ∧ ∑ i, w i • (pts i).toCircle.1 = 0

theorem problem :
    volume {pts | ContainsOrigin pts} / volume (@Set.univ (Fin 3 → UnitAddCircle)) = 1 / 4 := by
  sorry