Weird. It's not my field at all but intuitively, I would have approached a proof by trying to formalise the following:

1/ Complete part of the tiling in the upper right quadrant (this tiling exists by assumption)

2/ Shove all the tiles down and to the left

3/ Repeat.

It's very surprising that step 2 needs the axiom of choice. (Usually when I'm this surprised it means I've misunderstood something!)

Edit: your link proves something stronger - that the ability to tile an nxn square for all n is equivalent to tiling a quadrant and tiling a plane. I guess that's where choice comes in, is it?

That's what I meant by attempting to find a constructive proof. 2 doesn't work because no matter how much you shift down and to the left you'll always have a boundary.

> our link proves something stronger

No, it proves that the 3 statements are equivalent, so it is not stronger.

But isn't it enough to show that any point in the plane will eventually get tiled after 1 - 3 run for long enough?

Because surely all points do get tiled eventually by the method above.

This falls short of the original goal: While your method shows that for every point, you can find a tiling large enough that covers it, the original question was to find a single tiling covering everything.

Finding progressively larger, finite tilings is not the same as having a single infinite tiling, just like finding larger and larger natural numbers is not the same as having a single number larger than all natural numbers (which wouldn't be a natural number).

König's lemma implies that for tilings both statements are in fact equivalent.

> like finding larger and larger natural numbers is not the same as having a single number larger than all natural numbers

Very nice analogy!

> König's lemma implies that for tilings both statements are in fact equivalent.

Exactly, and instead of working by shifting the tiling (which would produce a sequence of incompatible tilings) it works by finding a sequence of finite tilings where each is a subset of the next, so it makes sense to take the union of the sequence.

With the caveat that if your tiling is inductive in the sense that the tiling of n+1 is an extension of n, a series of finite tilings will tile the plane.

Well, a naïve way to "prove" it would be to flip the quadrant over the axes to tile the other quadrants. Is this legal? Or, more specifically, are there tiles that can tile something one way, but not if flipped?

If you flip the quadrant you're also flipping the tiles. The flipped tiles may not be in your set.