The optimal paper Moebius band | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: R. E. Schwartz, `The optimal paper Moebius band`, Annals of Math, 201 (1) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2025-201-1-OptimalMoebius.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 (a : ℝ) (ha : a > 0) (f : ℝ² → ℝ³) (hf : OptimalMoebius.IsMoebiusEmbedding a f) :
    a > √3 := bya:ℝha:a > 0f:ℝ² → ℝ³hf:IsMoebiusEmbedding a f⊢ a > √3
  sorryAll goals completed! 🐙