A counterexample to the periodic tiling conjecture | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: R. Greenfeld and T. Tao, `A counterexample to the periodic tiling conjecture`, Annals of Math, 200 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2024-200-1-PeriodicTilingConjecture.lean

Informal solution: Unavailable.

/--
Statement of Theorem 1.4 (Counterexample to Conjecture 1.2, I):

There exists a finite abelian group `G₀` and a finite non-empty `F ⊆ ℤ² × G₀` such that
`F` forms an aperiodic tiling equation.
-/
theorem declaration uses `sorry`theorem_1_4 : ∃ (G₀ : Type) (_ : AddCommGroup G₀) (_ : Finite G₀),
    ∃ F : Set (ℤ × ℤ × G₀), F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F := by⊢ ∃ G₀ x, ∃ (_ : Finite G₀), ∃ F, F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F
  sorryAll goals completed! 🐙

/--
Statement of Corollary 1.6 (Counterexample to Conjecture 1.2, II):

For all sufficiently large `d`, there exists a finite non-empty `F ⊆ ℤᵈ` such that
`F` forms an aperiodic tiling equation.
-/
theorem declaration uses `sorry`corollary_1_6 : ∀ᶠ d in atTop, ∃ (F : Set (Fin d → ℤ)),
    F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F := by⊢ ∀ᶠ (d : ℕ) in atTop, ∃ F, F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F
  sorryAll goals completed! 🐙

/--
Statement of Corollary 1.7 (Counterexample to Conjecture 1.3):

For all sufficiently large `d`, there exists a bounded measurable set `σ ⊆ ℝᵈ` of positive
measure such that `σ` forms an aperiodic continuous tiling equation.
-/
theorem declaration uses `sorry`corollary_1_7 : ∀ᶠ d in atTop, ∃ σ : Set (Fin d → ℝ), IsBounded σ ∧ MeasurableSet σ ∧
    0 < volume σ ∧ IsAperiodicContinuousTilingEquation σ := by⊢ ∀ᶠ (d : ℕ) in atTop, ∃ σ, Bornology.IsBounded σ ∧ MeasurableSet σ ∧ 0 < volume σ ∧ IsAperiodicContinuousTilingEquation σ
  sorryAll goals completed! 🐙