1. FormalConjectures
  2. Wikipedia
  3. InscribedSquare
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Inscribed square problem

The inscribed square problem or Toeplitz conjecture asks whether every Jordan curve (i.e. simple close curve in ℝ²) admits an inscribed square, i.e. a square whose vertices all lie on the curve. There are several open and solved variants of this conjecture.

References:

open Topology ContDiff Manifoldopen scoped EuclideanGeometry namespace InscribedSquare

Four points a b c d in the plane form a rectangle with a opposite to c iff the line segments from a to c and from b to d have both the same length and the same midpoint, acting as the diagonals of the rectangle. We also require the rectangle to be nondegenerate and have a given aspect ratio ratio : ℝ.

structure IsRectangle (a b c d : ℝ²) (ratio : ℝ) : Prop where diagonal_midpoints_eq : a + c = b + d diagonal_lengths_eq : dist a c = dist b d a_ne_b : a ≠ b b_ne_c : b ≠ c has_ratio : (dist a b) / (dist b c) = ratio

Inscribed square problem Does every Jordan curve admit an inscribed square?

@[category research open, AMS 51] theorem declaration uses 'sorry'inscribed_square_problem : answer(sorry) ↔ ∀ (γ : Circle → ℝ²) (hγ : IsEmbedding γ), ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1 := ⊢ True ↔ ∀ (γ : Circle → ℝ²), IsEmbedding γ → ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1 All goals completed! 🐙

Inscribed rectangle problem Does every Jordan curve admit inscribed rectangles of any given aspect ratio?

@[category research open, AMS 51] theorem declaration uses 'sorry'inscribed_rectangle_problem : answer(sorry) ↔ ∀ (γ : Circle → ℝ²) (hγ : IsEmbedding γ) (r : ℝ) (hr : r > 0), ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r := ⊢ True ↔ ∀ (γ : Circle → ℝ²), IsEmbedding γ → ∀ r > 0, ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r All goals completed! 🐙

It is known that every Jordan curve admits at least one inscribed rectangle.

@[category research solved, AMS 51] theorem declaration uses 'sorry'exists_inscribed_rectangle (γ : Circle → ℝ²) (hγ : IsEmbedding γ) : ∃ t₁ t₂ t₃ t₄ r, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r := γ:Circle → ℝ²hγ:IsEmbedding γ⊢ ∃ t₁ t₂ t₃ t₄ r, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r All goals completed! 🐙

It is known that every smooth Jordan curve admits inscribed rectangles of all aspect ratios.

@[category research solved, AMS 51] theorem declaration uses 'sorry'exists_inscribed_rectangle_of_smooth (γ : Circle → ℝ²) (hγ : IsEmbedding γ) (hγ' : ContMDiff (𝓡 1) (𝓡 2) ∞ γ) (r : ℝ) (hr : r > 0) : ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r := γ:Circle → ℝ²hγ:IsEmbedding γhγ':ContMDiff (𝓡 1) (𝓡 2) ∞ γr:ℝhr:r > 0⊢ ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r All goals completed! 🐙

It is also known that every $C^2$ Jordan curve admits an inscribed square.

@[category research solved, AMS 51] theorem declaration uses 'sorry'exists_inscribed_square_of_C2 (γ : Circle → ℝ²) (hγ : IsEmbedding γ) (hγ' : ContMDiff (𝓡 1) (𝓡 2) 2 γ) : ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1 := γ:Circle → ℝ²hγ:IsEmbedding γhγ':ContMDiff (𝓡 1) (𝓡 2) 2 γ⊢ ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1 All goals completed! 🐙 end InscribedSquare