foobar__

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.

Both Isabelle and Coq are based on higher-order logics, so I am not sure how first-order logic is a barrier to entry. Especially Isabelle is very easy to use because the logic is so standard with nothing really surprising or especially restricting (a very strong form of the axiom of choice is deeply embedded in the system, so it's probably harder if you care about it at this level).

Regarding your second point, to me this looks pretty much the same as in software: In high-quality code I expect high-level comments that give me intuition about the code, and I also expect high-level documentation giving me further intuition about the components and the system as a whole. The more complicated the system is, the more important the comments and the documentation become.

I see no reason why we should hold computer-assisted proofs to a lesser standard.

I am not satisfied by picture proofs, I'd like to see derivations from axioms and known results.

I love pictures that give me intuition about a proof and I agree that intuition is crucial to understanding. But all the intuition in the world is useless if the proof fails because of one tiny logically unsound step or one pathological corner case, so it's no good to ignore the technical details or, even worse, to become unable to expand a purpoted proof one has written into a fully detailed version, which I suppose can easily happen if someone relies too much on intuition.

I find it unintuitive when the strength difference between the two players is too high, and I think matter-of-fact statements like in the stackoverflow answer ("Of course, a human assisting a computer player will be stronger than the same computer player alone") need to be questioned.

Imagine a beginner receiving suggested moves from a grandmaster. I can't see how this beginner could be stronger than the grandmaster alone, and they would almost certainly be weaker if they override just one of the grandmaster's suggestions.

From what I read, chess AIs are this far above humans.

Where did you find this information for chess? It sounds unintuitive that a superior player would benefit from a weak player's help.

Where are tubes faster than semiconductors?

They can easily look at the RAM of the VM and get the plain-text encryption keys for SSL or VPN or whatever.

I'm absolutely sure by now someone has written a program to automate this, and to be honest I expect some governments already force some companies to do this.

How is it better?

I don't think this would be good idea. Then there would be the danger of employers pressuring their employees to waive their rights: "If you insist on working only 11h/day, we can hire someone else."

I would totally expect this to happen for basically every minimum wage job if you could waive your rights like this.