From 1eb7fece7f1cba99ff989b1832d7d090bd0c3c4e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 May 2026 19:39:39 +0000 Subject: [PATCH] feat: add Schoenflies theorem eval problem MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §48 of Knill's "Some Fundamental Theorems in Mathematics" (Schoenflies, 1906). Strong form: every Jordan curve in the plane is the image of the unit circle under some self-homeomorphism of ℝ². Faithful encoding of Knill's prose statement that "each complementary region is homeomorphic to the open disk" — the strong form is the result that is actually true and implies the bounded-region claim. Mathlib has Metric.sphere, EuclideanSpace, and Homeomorph, but no Schoenflies theorem, no Jordan curve theorem, no invariance-of-domain machinery in a form that would discharge it. Stateable with zero new definitions. Co-Authored-By: Claude Opus 4.7 --- LeanEval/Topology/Schoenflies.lean | 41 +++++++++++++++++++++++++++++ manifests/problems/schoenflies.toml | 9 +++++++ 2 files changed, 50 insertions(+) create mode 100644 LeanEval/Topology/Schoenflies.lean create mode 100644 manifests/problems/schoenflies.toml diff --git a/LeanEval/Topology/Schoenflies.lean b/LeanEval/Topology/Schoenflies.lean new file mode 100644 index 0000000..5b6c224 --- /dev/null +++ b/LeanEval/Topology/Schoenflies.lean @@ -0,0 +1,41 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace Topology + +/-! +# Schoenflies theorem (Arthur Moritz Schoenflies, 1906) + +§48 of Knill's *Some Fundamental Theorems in Mathematics*. The strong +form: for every Jordan curve in the plane there is a self-homeomorphism +of `ℝ²` carrying the curve to the standard unit circle. + +This is the faithful encoding of Knill's prose statement that "each +complementary region is homeomorphic to the disk", which as +literally written is false for the unbounded region (homeomorphic to +`ℝ² ∖ closedBall 0 1`, fundamental group `ℤ`, vs. simply connected +disk). The strong form here implies that the bounded complementary +region is homeomorphic to the disk, recovering the correct half of +Knill's claim. + +Mathlib has `Metric.sphere`, `EuclideanSpace`, and `Homeomorph`, but +**no Schoenflies theorem** (`grep -ri 'schoenflies' Mathlib/`: no +hits), no Jordan curve theorem, and no associated invariance-of-domain +machinery in a form that would discharge it. Stateable with no new +definitions. +-/ + +/-- **Schoenflies theorem (strong form).** For every Jordan curve in +the plane there is a self-homeomorphism of `ℝ²` carrying the curve to +the standard unit circle. -/ +@[eval_problem] +theorem schoenflies + (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 → EuclideanSpace ℝ (Fin 2)) + (_hcont : Continuous r) (_hinj : Function.Injective r) : + ∃ h : EuclideanSpace ℝ (Fin 2) ≃ₜ EuclideanSpace ℝ (Fin 2), + h '' Set.range r = Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by + sorry + +end Topology +end LeanEval diff --git a/manifests/problems/schoenflies.toml b/manifests/problems/schoenflies.toml new file mode 100644 index 0000000..a3d1fbb --- /dev/null +++ b/manifests/problems/schoenflies.toml @@ -0,0 +1,9 @@ +id = "schoenflies" +title = "Schoenflies theorem" +test = false +module = "LeanEval.Topology.Schoenflies" +holes = ["schoenflies"] +submitter = "Kim Morrison" +notes = "§48 of Knill's 'Some Fundamental Theorems in Mathematics'. Strong form: every Jordan curve in the plane is the image of the unit circle under some self-homeomorphism of ℝ². This is the faithful encoding of Knill's prose statement 'each complementary region is homeomorphic to the open disk' — which as literally written is false for the unbounded region (homeomorphic to ℝ² ∖ closedBall 0 1, fundamental group ℤ, not simply connected). The strong form implies the bounded region is homeomorphic to the open disk. Mathlib has Metric.sphere, EuclideanSpace, and Homeomorph, but no Schoenflies theorem (`grep -ri 'schoenflies' Mathlib/`: no hits), no Jordan curve theorem, no invariance-of-domain machinery in a form that would discharge it. Stateable with zero new definitions." +source = "A. M. Schoenflies, *Beiträge zur Theorie der Punktmengen III*, Math. Annalen 62 (1906) (first proof, with gaps); rigorous proofs by L. Antoine (1921), L. E. J. Brouwer (1909–10). Listed as §48 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover." +informal_solution = "Classical proof: (i) the Jordan curve theorem gives the inside and outside regions; (ii) Riemann mapping for the bounded inside extends to a homeomorphism of the closed disk by Carathéodory's theorem on prime ends; (iii) a parallel construction handles the outside; (iv) the two homeomorphisms patch along the curve to a homeomorphism of ℝ²."