4 ms·

One of the coolest things about the hat tile is that it was discovered by a hobbyist playing with puzzle software. There's a great Quanta story about this: http

by necubi 3y ago

One of the coolest things about the hat tile is that it was discovered by a hobbyist playing with puzzle software. There's a great Quanta story about this: https://www.quantamagazine.org/hobbyist-finds-maths-elusive-einstein-tile-20230404/ https://www.quantamagazine.org/hobbyist-finds-maths-elusive-....

yboris 3y ago
There's a great video explanation too with interviews of people behind the scenes: https://youtu.be/4HHUGnHcDQw?si=APHEQwVxTvcOfC5c&t=382 https://youtu.be/4HHUGnHcDQw?si=APHEQwVxTvcOfC5c&t=382
nhatcher 3y ago
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/ https://www.nhatcher.com/post/on-hats-and-sats/
- OscarCunningham 3y ago
  If they found the material properties of that tile, they would be doing 'spectroscopy'.
QuadmasterXLII 3y ago
Jim's blog post about his discovery is also delightful to read: https://hedraweb.wordpress.com/2023/03/23/its-a-shape-jim-but-not-as-we-know-it/ 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/ https://www.hgreer.com/HatTile/
- NooneAtAll3 3y ago
  > using a SAT solver (in this case, Z3) isn't z3 SMT solver, not SAT?
  - nhatcher 3y ago
    Z3 has both, but the tool they are using is the SAT solver.
- nhatcher 3y ago
  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

by necubi 3y ago

yboris 3y ago

There's a great video explanation too with interviews of people behind the scenes: https://youtu.be/4HHUGnHcDQw?si=APHEQwVxTvcOfC5c&t=382 https://youtu.be/4HHUGnHcDQw?si=APHEQwVxTvcOfC5c&t=382

nhatcher 3y ago

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/ https://www.nhatcher.com/post/on-hats-and-sats/

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

QuadmasterXLII 3y ago

Jim's blog post about his discovery is also delightful to read: https://hedraweb.wordpress.com/2023/03/23/its-a-shape-jim-but-not-as-we-know-it/ 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/ https://www.hgreer.com/HatTile/

NooneAtAll3 3y ago
> using a SAT solver (in this case, Z3) isn't z3 SMT solver, not SAT?
- nhatcher 3y ago
  Z3 has both, but the tool they are using is the SAT solver.
nhatcher 3y ago
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