feat(Wikipedia): Fuglede's conjecture

[aditya-ramabadran]

Formalized Fuglede's conjecture (in dims 1 and 2):

A bounded subset of $\mathbb R$ (resp. $\mathbb R^2$) with positive Lebesgue measure is spectral iff it tiles $\mathbb R$ (resp. $\mathbb R^2$) by translation.

• Closes Fuglede's conjecture: spectral sets and tilings #3476
• Used Gemini sparingly to investigateMeasureTheory.MemLp and simplify formalization of expFunction_is_L2

[aditya-ramabadran]

Also a note: there are other open problems and conjectures in the area of Fuglede's conjecture and spectral sets and (weak/strong) tiling, for example in the following papers: https://arxiv.org/pdf/2209.04540, https://arxiv.org/pdf/2506.23631, https://arxiv.org/pdf/2408.15361.

So if we want to formalize these as well, it might be useful to put the definitions / lemmas about spectral sets in some shared area, I'm not sure how this would work or where they could go or the best way to organize all this, open to any advice on that.

Some example conjectures/open problems from those papers: (should I create issues for each one? or maybe multiple in the same issue?)

• Bounded nowhere dense set of positive measure in $\mathbb{R}^d$: can it be spectral? (open for $d \ge 2$)

• Let $\Omega = A \times B$ where $A$ is a convex body in $\mathbb{R}^n$ and $B$ is a bounded measurable set in $\mathbb{R}^m$. If $\Omega$ is spectral, must $B$ be spectral?

• Let $K$ be a convex body in $\mathbb{R}^d$, and let $W(K)$ be the set of positive locally finite measures $\nu$ such that $1_K * \nu = 1_{K^c}$ a.e. Is every extremal point of $W(K)$ a proper tiling?

• Let $\Omega \subset \mathbb{R}$ be a finite union of intervals, and let $\nu$ be a weak tiling measure for $\Omega$. Must $\text{supp}(\nu)$ have bounded density?

• Let $\Omega \subset \mathbb{R}$ be a finite union of three or more intervals. If $\Omega$ weakly tiles its complement, must it also tile properly?

• Let $\Omega \subset \mathbb{R}$ be a finite union of intervals, and let $\nu$ be a weak tiling measure for $\Omega$. Must $\nu$ be a convex linear combination of proper tilings?

• Let $E \subset \mathbb{R}$ be a bounded spectral set. Is its spectrum $\Lambda$ necessarily rational? More generally, does every spectral $E$ admit some rational spectrum?

[franzhusch]

We have the folder FormalConjecturesForMathlib for shared definitions.

About creating one issue or multiple issues, I would say it depends on the effort / difficulty and how close the conjectures are to each other / if it would make sense to put them all into one file anyway.

[franzhusch]

Small Note on Fuglede's Conjecture, you can also add the negative answer for the dimension d > 2 cases as category research solved. Research Solved problems can act as a autoformalization benchmark.

[aditya-ramabadran]

Makes sense, thanks! I'll add the issues and the negative answer for $d>2$, and move the shared definitions to a new file