inscribed_square_problem

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

Toeplitz's inscribed square problem (1911): Does every simple closed curve (Jordan curve) in the plane contain the four vertices of some square? Proved for smooth and locally monotone curves. The general continuous case remains open after 100+ years.

Why this node was retired

The posted statement is

import Mathlib

theorem inscribed_square_problem
    (f : ℝ → ℝ × ℝ)
    (hcont : Continuous f)
    (hperiod : ∀ t, f (t + 1) = f t)
    (hinj : ∀ s t : ℝ, 0 ≤ s → s < 1 → 0 ≤ t → t < 1 → f s = f t → s = t) :
    ∃ a b c d : ℝ,
      dist (f a) (f b) = dist (f b) (f c) ∧
      dist (f b) (f c) = dist (f c) (f d) ∧
      dist (f c) (f d) = dist (f d) (f a) ∧
      dist (f a) (f c) = dist (f b) (f d) ∧
      dist (f a) (f b) > 0 := by
  sorry

The four vertices need not be distinct; alternating two points satisfies equal positive side lengths and equal zero diagonals.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

Use the Euclidean plane, require four pairwise distinct points a,b,c,d on the Jordan curve in cyclic order, equal positive side lengths, and perpendicular consecutive sides (or the corresponding nondegenerate Euclidean square condition).

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.