The rectangular peg problem | Lean AI formalization leaderboard

Problem statement

Notes: LeanEval renames upstream's declaration `theorem «theorem»` to `theorem_1` because the workspace generator cannot address a declaration whose basename is a reserved word; the statement is unchanged.

Source: J. E. Greene and A. Lobb, `The rectangular peg problem`, Annals of Math, 194 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-194-2-RectangularPegProblem.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1 (γ : Circle → ℂ) (z w : ℂ) (θ : Real.Angle)
    (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℂ) ∞ γ) :
    ∃ (θ' : Real.Angle), ∃ (z' w' : ℂ), Similar (R z w θ) (R z' w' θ') ∧
    ∀ i : Fin 4, R z' w' θ' i ∈ Set.range γ := byγ:Circle → ℂz:ℂw:ℂθ:Anglehγ:IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℂ) ∞ γ⊢ ∃ θ' z' w', Similar (R z w θ) (R z' w' θ') ∧ ∀ (i : Fin 4), R z' w' θ' i ∈ Set.range γ
  sorryAll goals completed! 🐙