[flaubere]

It looks like many of these show a construction which you have to follow the details of to check that there aren't gaps or overlaps.

Is there a way of checking these automatically? Eg if you can tile a certain amount of space without gaps then it must be able to continue forever? Or can you write down a vector expression for the location of each shape and show finitely that you have exactly covered all lattice points?

[zodiac]

I think the "answer to q2" here (https://mathoverflow.net/questions/199097/which-unfoldings-o...) is what you want!

[ironSkillet]

It does seem like there's an underlying combinatorial nature to all of these proofs that might make them amenable to a computer based proof. A brute force approach might even work here since everything is based on a lattice. Enumerate amalgamations with a bounded # of pieces, check for tile-ability either by brute force or some clever trick. Rinse and repeat on a breadth first search basis across all shapes, and eventually you'll either prove that all shapes work or the program will run for an unbounded amount of time and you'll prove that "no tiling exists consisting of less than X pieces for this shape Y"