From a91e62c02b8ebe7db4ac06d99fb98fdd34a2b770 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Fri, 11 Sep 2026 05:02:58 +0800
Subject: [PATCH 1/2] feat(Geometry): aperiodic monotiles

---
 LeanEval/Geometry/AperiodicMonotiles.lean   | 79 +++++++++++++++++++++
 manifests/problems/aperiodic_monotiles.toml | 15 ++++
 2 files changed, 94 insertions(+)
 create mode 100644 LeanEval/Geometry/AperiodicMonotiles.lean
 create mode 100644 manifests/problems/aperiodic_monotiles.toml

diff --git a/LeanEval/Geometry/AperiodicMonotiles.lean b/LeanEval/Geometry/AperiodicMonotiles.lean
new file mode 100644
index 00000000..3cd459a3
--- /dev/null
+++ b/LeanEval/Geometry/AperiodicMonotiles.lean
@@ -0,0 +1,79 @@
+import Mathlib
+import EvalTools.Markers
+
+/-!
+# Aperiodic monotiles
+
+References:
+
+David Smith, Joseph Samuel Myers, Craig S. Kaplan, Chaim Goodman-Strauss.
+An aperiodic monotile, https://arxiv.org/abs/2303.10798
+A chiral aperiodic monotile, https://arxiv.org/abs/2305.17743
+-/
+
+namespace LeanEval.Geometry.AperiodicMonotiles
+
+/-- A topological tiling of a topological space is a collection of subsets (tiles) with
+pairwise disjoint interiors such that the union of the closures is the whole space. -/
+structure TopologicalTiling (X : Type*) [TopologicalSpace X] : Type _ where
+  sets : Set (Set X)
+  disjoint : sets.Pairwise fun s t ↦ Disjoint (interior s) (interior t)
+  union_eq_univ : ⋃₀ (closure '' sets) = .univ
+
+/-- A tiling of a metric space X by another metric space T is a topological tiling in
+which all tiles are isometric copies of T. -/
+structure TilingBy (T X : Type*) [PseudoEMetricSpace T] [PseudoEMetricSpace X]
+    extends TopologicalTiling X where
+  isometry : ∀ s ∈ sets, ∃ f : T → X, Isometry f ∧ s = .range f
+
+/-- The vectors from one boundary vertex to the next (in counterclockwise order)
+of the tile Tile(a,b) defined in the paper. -/
+noncomputable def vec (a b : NNReal) : Fin 13 → ℝ × ℝ :=
+  ![a • (2,0), a • (1,√3) / 2, b • (√3,-1) / 2, b • (√3,1) / 2, a • (-1,√3) / 2, a • (-1,0),
+    b • (0,1), b • (-√3,1) / 2, a • (-1,-√3) / 2, a • (-1,0), b • (0,-1), b • (-√3,-1) / 2,
+    a • (1,-√3) / 2]
+
+/-- The Euclidean plane. -/
+abbrev Plane := EuclideanSpace ℝ (Fin 2)
+
+/-- Construct a point in the Euclidean plane from a pair of real numbers. -/
+def toPlane (x : ℝ × ℝ) : Plane := .toLp (p := 2) ![x.1, x.2]
+
+/-- The boundary vertices (in counterclockwise order) of Tile(a,b). -/
+noncomputable def vertex (a b : NNReal) (i : Fin 13) : Plane :=
+  toPlane <| ∑ j ∈ Finset.Ioi i, vec a b j
+
+/-- The boundary polygon of Tile(a,b). -/
+def polygon (a b : NNReal) : Set Plane :=
+  ⋃ i : ZMod 13, convexHull ℝ {vertex a b i, vertex a b (i + 1 : ZMod 13)}
+
+/-- The tile Tile(a,b), which is the closure of the bounded component of the complement of
+the boundary polygon. Notice that (a, √3/2*a) always lies in the bounded component. -/
+def tile (a b : NNReal) : Set Plane :=
+  closure <| connectedComponentIn (polygon a b)ᶜ (.toLp (p := 2) ![a, √3/2*a])
+
+/-- A chiral tiling of the Euclidean plane by Tile(a,b) consists of tiles that are images
+of Tile(a,b) under orientation preserving isometries of the plane. -/
+structure ChiralTilingBy (a b : NNReal) extends TopologicalTiling Plane where
+  isometry : ∀ s ∈ sets, ∃ f : Plane →ᵃ[ℝ] Plane, Isometry f ∧ f.linear.det = 1 ∧ s = f '' tile a b
+
+/-- A collection of sets is aperiodic if it is not invariant under any nontrivial translation. -/
+def IsAperiodic {X : Type*} [AddZeroClass X] (S : Set (Set X)) : Prop :=
+  ∀ x : X, (Set.image (· + x)) '' S = S → x = 0
+
+/-- The main theorem of *An aperiodic monotile*: if a and b are distinct positive real numbers,
+then the Euclidean plane admits tilings by Tile(a,b), but only aperiodic ones. -/
+@[eval_problem]
+theorem isAperiodic_tilingBy (a b : NNReal) (ha : a ≠ 0) (hb : b ≠ 0) (ne : a ≠ b) :
+    Nonempty (TilingBy (tile a b) Plane) ∧
+    ∀ t : TilingBy (tile a b) Plane, IsAperiodic t.sets := by
+  sorry
+
+/-- One of the main theorem of *A chiral aperiodic monotile*: the Euclidean plane admits chiral
+tilings by Tile(1,1), but only aperiodic ones. -/
+@[eval_problem]
+theorem isAperiodic_chiralTilingBy :
+    Nonempty (ChiralTilingBy 1 1) ∧ ∀ t : ChiralTilingBy 1 1, IsAperiodic t.sets := by
+  sorry
+
+end LeanEval.Geometry.AperiodicMonotiles
diff --git a/manifests/problems/aperiodic_monotiles.toml b/manifests/problems/aperiodic_monotiles.toml
new file mode 100644
index 00000000..8fe7ea9c
--- /dev/null
+++ b/manifests/problems/aperiodic_monotiles.toml
@@ -0,0 +1,15 @@
+id = "aperiodic_monotiles"
+title = "Aperiodic monotiles"
+group = "formalization-evaluation"
+status = "active"
+visible = true
+statement_revision = 1
+tags = []
+module = "LeanEval.Geometry.AperiodicMonotiles"
+holes = ["isAperiodic_tilingBy", "isAperiodic_chiralTilingBy"]
+submitter = "Junyan Xu"
+
+[[status_history]]
+status = "active"
+effective_date = "2026-09-11"
+reason = "policy"

From 1641efd6dd652b9008e36d1fdfb44674527552b8 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Sat, 12 Sep 2026 01:53:50 +0800
Subject: [PATCH 2/2] improvements

---
 LeanEval/Geometry/AperiodicMonotiles.lean   | 46 +++++++++++----------
 manifests/problems/aperiodic_monotiles.toml |  2 +-
 2 files changed, 25 insertions(+), 23 deletions(-)

diff --git a/LeanEval/Geometry/AperiodicMonotiles.lean b/LeanEval/Geometry/AperiodicMonotiles.lean
index 3cd459a3..ea24df12 100644
--- a/LeanEval/Geometry/AperiodicMonotiles.lean
+++ b/LeanEval/Geometry/AperiodicMonotiles.lean
@@ -4,7 +4,7 @@ import EvalTools.Markers
 /-!
 # Aperiodic monotiles
 
-References:
+## References
 
 David Smith, Joseph Samuel Myers, Craig S. Kaplan, Chaim Goodman-Strauss.
 An aperiodic monotile, https://arxiv.org/abs/2303.10798
@@ -27,11 +27,11 @@ structure TilingBy (T X : Type*) [PseudoEMetricSpace T] [PseudoEMetricSpace X]
   isometry : ∀ s ∈ sets, ∃ f : T → X, Isometry f ∧ s = .range f
 
 /-- The vectors from one boundary vertex to the next (in counterclockwise order)
-of the tile Tile(a,b) defined in the paper. -/
+of the tile Tile(𝑎,𝑏) defined in the paper. -/
 noncomputable def vec (a b : NNReal) : Fin 13 → ℝ × ℝ :=
-  ![a • (2,0), a • (1,√3) / 2, b • (√3,-1) / 2, b • (√3,1) / 2, a • (-1,√3) / 2, a • (-1,0),
-    b • (0,1), b • (-√3,1) / 2, a • (-1,-√3) / 2, a • (-1,0), b • (0,-1), b • (-√3,-1) / 2,
-    a • (1,-√3) / 2]
+  ![a • (2,0), a • (1/2,√3/2), b • (√3/2,-1/2), b • (√3/2,1/2), a • (-1/2,√3/2), a • (-1,0),
+    b • (0,1), b • (-√3/2,1/2), a • (-1/2,-√3/2), a • (-1,0), b • (0,-1), b • (-√3/2,-1/2),
+    a • (1/2,-√3/2)]
 
 /-- The Euclidean plane. -/
 abbrev Plane := EuclideanSpace ℝ (Fin 2)
@@ -39,41 +39,43 @@ abbrev Plane := EuclideanSpace ℝ (Fin 2)
 /-- Construct a point in the Euclidean plane from a pair of real numbers. -/
 def toPlane (x : ℝ × ℝ) : Plane := .toLp (p := 2) ![x.1, x.2]
 
-/-- The boundary vertices (in counterclockwise order) of Tile(a,b). -/
+/-- The boundary vertices (in counterclockwise order) of Tile(𝑎,𝑏). -/
 noncomputable def vertex (a b : NNReal) (i : Fin 13) : Plane :=
   toPlane <| ∑ j ∈ Finset.Ioi i, vec a b j
 
-/-- The boundary polygon of Tile(a,b). -/
+/-- The boundary polygon of Tile(𝑎,𝑏). Notice that 12 + 1 = 0 in Fin 13. -/
 def polygon (a b : NNReal) : Set Plane :=
-  ⋃ i : ZMod 13, convexHull ℝ {vertex a b i, vertex a b (i + 1 : ZMod 13)}
+  ⋃ i : Fin 13, segment ℝ (vertex a b i) (vertex a b (i + 1))
 
-/-- The tile Tile(a,b), which is the closure of the bounded component of the complement of
-the boundary polygon. Notice that (a, √3/2*a) always lies in the bounded component. -/
+/-- The tile Tile(𝑎,𝑏), which is the closure of the bounded component of the complement of
+the boundary polygon. Notice that the open segment between the 2nd vertex (5𝑎/2, √3𝑎/2) and the
+6th vertex (𝑎+√3𝑏, √3𝑎) always lies in the bounded component, even when one of 𝑎 and 𝑏 is 0.
+The tile could also be decomposed into 6 smaller polygons, 5 of which are convex, see
+https://www.desmos.com/calculator/2tcx1o6uoy. -/
 def tile (a b : NNReal) : Set Plane :=
-  closure <| connectedComponentIn (polygon a b)ᶜ (.toLp (p := 2) ![a, √3/2*a])
+  closure <| connectedComponentIn (polygon a b)ᶜ (midpoint ℝ (vertex a b 2) (vertex a b 6))
 
-/-- A chiral tiling of the Euclidean plane by Tile(a,b) consists of tiles that are images
-of Tile(a,b) under orientation preserving isometries of the plane. -/
+/-- A chiral tiling of the Euclidean plane by Tile(𝑎,𝑏) consists of tiles that are images
+of Tile(𝑎,𝑏) under orientation preserving isometries of the plane. -/
 structure ChiralTilingBy (a b : NNReal) extends TopologicalTiling Plane where
   isometry : ∀ s ∈ sets, ∃ f : Plane →ᵃ[ℝ] Plane, Isometry f ∧ f.linear.det = 1 ∧ s = f '' tile a b
 
 /-- A collection of sets is aperiodic if it is not invariant under any nontrivial translation. -/
-def IsAperiodic {X : Type*} [AddZeroClass X] (S : Set (Set X)) : Prop :=
+def Aperiodic {X : Type*} [AddZeroClass X] (S : Set (Set X)) : Prop :=
   ∀ x : X, (Set.image (· + x)) '' S = S → x = 0
 
-/-- The main theorem of *An aperiodic monotile*: if a and b are distinct positive real numbers,
-then the Euclidean plane admits tilings by Tile(a,b), but only aperiodic ones. -/
+/-- The main theorem from *An aperiodic monotile*: if 𝑎 and 𝑏 are distinct positive real numbers,
+then the Euclidean plane admits tilings by Tile(𝑎,𝑏), but only aperiodic ones. -/
 @[eval_problem]
-theorem isAperiodic_tilingBy (a b : NNReal) (ha : a ≠ 0) (hb : b ≠ 0) (ne : a ≠ b) :
-    Nonempty (TilingBy (tile a b) Plane) ∧
-    ∀ t : TilingBy (tile a b) Plane, IsAperiodic t.sets := by
+theorem aperiodic_tilingBy (a b : NNReal) (ha : a ≠ 0) (hb : b ≠ 0) (ne : a ≠ b) :
+    Nonempty (TilingBy (tile a b) Plane) ∧ ∀ t : TilingBy (tile a b) Plane, Aperiodic t.sets := by
   sorry
 
-/-- One of the main theorem of *A chiral aperiodic monotile*: the Euclidean plane admits chiral
+/-- One of the main theorems from *A chiral aperiodic monotile*: the Euclidean plane admits chiral
 tilings by Tile(1,1), but only aperiodic ones. -/
 @[eval_problem]
-theorem isAperiodic_chiralTilingBy :
-    Nonempty (ChiralTilingBy 1 1) ∧ ∀ t : ChiralTilingBy 1 1, IsAperiodic t.sets := by
+theorem aperiodic_chiralTilingBy :
+    Nonempty (ChiralTilingBy 1 1) ∧ ∀ t : ChiralTilingBy 1 1, Aperiodic t.sets := by
   sorry
 
 end LeanEval.Geometry.AperiodicMonotiles
diff --git a/manifests/problems/aperiodic_monotiles.toml b/manifests/problems/aperiodic_monotiles.toml
index 8fe7ea9c..e3bdf332 100644
--- a/manifests/problems/aperiodic_monotiles.toml
+++ b/manifests/problems/aperiodic_monotiles.toml
@@ -6,7 +6,7 @@ visible = true
 statement_revision = 1
 tags = []
 module = "LeanEval.Geometry.AperiodicMonotiles"
-holes = ["isAperiodic_tilingBy", "isAperiodic_chiralTilingBy"]
+holes = ["aperiodic_tilingBy", "aperiodic_chiralTilingBy"]
 submitter = "Junyan Xu"
 
 [[status_history]]