[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"