The Hopf Umlaufsatz (theorem of turning tangents) | Lean AI formalization leaderboard

Problem statement

Notes: A positively oriented simple closed unit-speed plane curve has total signed curvature 2π. Trusted helpers (signedArea, signedCurvature, totalCurvature, IsPositiveSimpleClosedUnitSpeedCurve, IsTangentAngleLift, …) are non-holes. Mathlib has no turning-tangents theorem. Candidate from §170 of the Knill survey.

Source: H. Hopf, *Über die Drehung der Tangenten...*, Compositio Math. 2 (1935). Knill, §170.

Informal solution: Unavailable.

theorem declaration uses `sorry`hopf_umlaufsatz {r : ℝ → LeanEval.Geometry.HopfUmlaufsatz.Plane} {α : ℝ → ℝ}
    (_hr : LeanEval.Geometry.HopfUmlaufsatz.IsPositiveSimpleClosedUnitSpeedCurve r)
    (_hα : LeanEval.Geometry.HopfUmlaufsatz.IsTangentAngleLift r α) :
    totalCurvature α = 2 * Real.pi := byr:ℝ → Planeα:ℝ → ℝ_hr:IsPositiveSimpleClosedUnitSpeedCurve r_hα:IsTangentAngleLift r α⊢ totalCurvature α = 2 * Real.pi
  sorryAll goals completed! 🐙