An Aperiodic Monotile

Stream: maths

[David Michael Roberts]

Just thought I'd drop this here: David Smith, Joseph Samuel Myers, Craig S. Kaplan, Chaim Goodman-Strauss, An aperiodic monotile, https://arxiv.org/abs/2303.10798. The proof uses non-formal computer assistance, and might be something for a possibly ambitious project to formalise

Other resources:

• authors' page with interactive resources
• their gzipped Python code of the software verification part
• easy blog write-up for the general public
• SVG using approximate coordinates of vertices (and exact in comments)
• Christian Lawson-Perfect's repo for the original file for the above, and other formats, such as STL

[Joseph Myers]

I hope to work on a formal version eventually. Not before the Lean 4 transition is done, and I suspect late 2024 (or later) will be more convenient for starting work on this than late 2023.

[Joseph Myers]

Note that the proof of aperiodicity in section 3 does not depend at all on computer assistance. However, formalizing all the main results would include formalizing the classification of all tilings by these tiles (thus including the computer-assisted section 4), and since that classification also proves aperiodicity, formalizing the methods of section 3 might not actually yield any additional formalized results.

[Joseph Myers]

The nominally human-verifiable version of the computer case analysis in Appendix B is definitely more of an outline of how that case analysis could be accomplished in a reasonable amount of computer-generated Lean than something humans are actually likely to read in practice.

[Joseph Myers]

Note also that I'm pretty sure that some of the geometrical parts of the proof, and the link between those and combinatorial parts (e.g. Appendix A), would probably end up using obvious-to-humans observations about tilings and plane geometry and topology that, once stated in properly general mathlib-suitable form, end up depending on the Jordan curve theorem (or possibly related results or variants such as Jordan-Schoenflies). And I don't think I'm the right person to formalize the Jordan curve theorem and related results in a mathlib-suitable way. Adding such results to mathlib(4) might be a sensible project that would be of use in its own right beyond also being a helpful preliminary to formalizing this paper.

[Joseph Myers]

The references to [GS09, Lemma 1.1] (as a justification for local combinatorial descriptions of tilings producing geometrical tilings of the whole plane; the correct formal lemma statement would probably not be a literal copy of that lemma) also implicitly bring in a lot of theory about manifolds that again I wouldn't be the right person to formalize.
lemma1.1.png

[Joseph Myers]

Although in that case, I think it should be possible to prove a version of the lemma about combinatorial tilings yielding geometrical tilings that's based on properties of covering spaces rather than needing so much theory of manifolds, which might also be more convenient to use. ([GS09, Lemma 1.1] was simply a convenient reference to use for this idea for linking combinatorial and geometrical tilings, Chaim thinks it actually dates back to the 19th century.)

[Joseph Myers]

Certainly I expect the more geometrical parts (e.g. Appendix A) to be much more work to formalize than the more combinatorial parts.

[Joseph Myers]

If anyone has work on combinatorial maps in Lean, that would be good to get into mathlib; I suspect combinatorial maps or similar will be convenient for formal reasoning about the substitution system (the arguments of section 5).

[Joseph Myers]

Simply proving that the family of tiles described in section 6 exist as topological disks is the sort of thing that's much simpler for humans than as a formal result. If you define the tiles by their boundaries, proving the boundary of a 13-gon is non-self-intersecting involves checking inequalities for 78 pairs of distinct sides, and while those inequalities are morally the sort of thing one might hope linarith to deal with, $\sqrt{3}$ is not something linarith would handle as a constant, so it probably can't actually handle most of those 78 sets of inequalities.

[Yaël Dillies]

As usual, the combinatorics is easy, but most of the combinatorics argument isn't actually combinatorics. This is a recurring theme that stopped Bhavik and I's formalisation of Sperner's lemma (branch#sperner-again).

[Yaël Dillies]

I think this project is a bit too ambitious at the moment, and time would be better spent on the prerequisites than on the paper itself.

[Patrick Massot]

Yaël Dillies said:

As usual, the combinatorics is easy, but most of the combinatorics argument isn't actually combinatorics. This is a recurring theme that stopped Bhavik and I's formalisation of Sperner's lemma (branch#sperner-again).

Could you elaborate on this?

[Yaël Dillies]

For Sperner, the whole proof is labelled combinatorics, but it crucially uses that an edge of a triangulation belongs to exactly two triangles if it's in the interior, and to exactly one triangle if it's on the boundary. This is actually false for general triangulations (you can have edges in the interior that only belong to one triangle), and you need the triangulation to be locally finite.

[Patrick Massot]

Interesting.

[Patrick Massot]

What does the one-edge counter-example look like?

[Yaël Dillies]

Take an edge $[AB]$ on a triangle $ABC$, a sequence $(D_n)$ of points outside the triangle converging to a point on $[AB]$, with further $D_{n + 1} ∈ ABD_n$. Then consider the triangulation made of $ABC$, $AD_nD_{n + 1}$, $BD_nD_{n + 1}$. Every point near $[AB]$ is either in $ABC$ or eventually gets swallowed by one of the small triangles. But the only triangle having $[AB]$ as an edge is $ABC$.

[Patrick Massot]

Ok, thanks

[David Michael Roberts]

@Joseph Myers thanks for your comments!