What is the conjecture
Let $\Omega \subset \mathbb{R}^d$ be a bounded measurable set with positive Lebesgue measure. A set $\Omega$ is spectral if the Hilbert space $L^2(\Omega)$ admits an orthogonal basis consisting of exponential functions ${e^{2\pi i \lambda \cdot x} : \lambda \in \Lambda}$ for some discrete set $\Lambda \subset \mathbb{R}^d$. A set $\Omega$ tiles $\mathbb{R}^d$ by translations if there exists a countable set $T \subset \mathbb{R}^d$ such that the sets ${\Omega + t : t \in T}$ partition $\mathbb{R}^d$ almost everywhere (i.e., their union is $\mathbb{R}^d$ and pairwise intersections have measure zero).
Fuglede's Conjecture (1974): A bounded measurable set $\Omega \subset \mathbb{R}^d$ is spectral if and only if it tiles $\mathbb{R}^d$ by translations.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 2/5 (0 is best) (as of 2026-03-08)
Building blocks (from Mathlib):
MeasureTheory.measure_prod_add_same and related measure theory infrastructure for handling translates of measurable setsPiLp and Hilbert space theory with orthonormal bases in InnerProductSpace.PiLp- Exponential functions and character theory in harmonic analysis
Missing pieces:
- Formal definition of "spectral set" as a bounded measurable set whose $L^2$ space admits an exponential orthonormal basis with specified index set
- Formal definition of "tiling by translations" capturing the partition property with countable translates
Rating justification: Core measure-theoretic and functional-analytic infrastructure exists in Mathlib (measures, $L^2$ spaces, orthonormal bases, exponential families). The main work is formalizing the specific definitions of spectral and tiling, which are moderate abstractions over existing concepts."
Choose either option
This issue was generated by an AI agent and reviewed by me.
If you have feedback on mistakes / hallucinations, feel free to just write it in the issue.See more information here: link
What is the conjecture
Let$\Omega \subset \mathbb{R}^d$ be a bounded measurable set with positive Lebesgue measure. A set $\Omega$ is spectral if the Hilbert space $L^2(\Omega)$ admits an orthogonal basis consisting of exponential functions ${e^{2\pi i \lambda \cdot x} : \lambda \in \Lambda}$ for some discrete set $\Lambda \subset \mathbb{R}^d$ . A set $\Omega$ tiles $\mathbb{R}^d$ by translations if there exists a countable set $T \subset \mathbb{R}^d$ such that the sets ${\Omega + t : t \in T}$ partition $\mathbb{R}^d$ almost everywhere (i.e., their union is $\mathbb{R}^d$ and pairwise intersections have measure zero).
Fuglede's Conjecture (1974): A bounded measurable set$\Omega \subset \mathbb{R}^d$ is spectral if and only if it tiles $\mathbb{R}^d$ by translations.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 2/5 (0 is best) (as of 2026-03-08)
Building blocks (from Mathlib):
MeasureTheory.measure_prod_add_sameand related measure theory infrastructure for handling translates of measurable setsPiLpand Hilbert space theory with orthonormal bases inInnerProductSpace.PiLpMissing pieces:
Rating justification: Core measure-theoretic and functional-analytic infrastructure exists in Mathlib (measures,$L^2$ spaces, orthonormal bases, exponential families). The main work is formalizing the specific definitions of spectral and tiling, which are moderate abstractions over existing concepts."
AMS categories
Choose either option
This issue was generated by an AI agent and reviewed by me.
If you have feedback on mistakes / hallucinations, feel free to just write it in the issue.See more information here: link