There's a great video explanation too with interviews of people behind the scenes:

https://youtu.be/4HHUGnHcDQw?si=APHEQwVxTvcOfC5c&t=382

I find it fascinating. It is inspiring and humbling. Not only he found the hat, he found also a different shape "the turtle". Basically out of thin air and then how they combine those two to find a real monotile. I am writing a bit about this:

https://www.nhatcher.com/post/on-hats-and-sats/

If they found the material properties of that tile, they would be doing 'spectroscopy'.

Jim's blog post about his discovery is also delightful to read: https://hedraweb.wordpress.com/2023/03/23/its-a-shape-jim-bu...

His offhand mention of "Craig's SAT Solver" opened a rabbit hole for me. I put together a blog post on how to draw the tiling without knowing the recursive structure by just feeding the shape into z3: https://www.hgreer.com/HatTile/

> using a SAT solver (in this case, Z3)

isn't z3 SMT solver, not SAT?

Z3 has both, but the tool they are using is the SAT solver.

Hi @QuadmasterXLII, you linked my blog in yours! Thanks, I feel honored! I found your blog halfway going through my own rabbit whole. I think had I seen it before embarking into the project I would have just use yours. That being said it is been a fun ride. It's interesting that we both got triggered by "Craig's SAT solver". Thanks again,

Nicolás