HN user
Sadly, the images for non-commercial use appear to be restricted to a medium resolution with high JPEG compression artifacts [1].
As an example I downloaded the image https://www.britishmuseum.org/collection/image/1613717051 (~1 MB, 2500x1973).
Still good enough for many use cases, but it limits personal prints.
[1] https://www.britishmuseum.org/terms-use/copyright-and-permis...
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.
Interestingly, the official website doesn't mention climate change at all, as far as I can see [1].
Instead, it claims that the purpose of the tunnels is to protect the areas surrounding some smaller rivers upstream of Tokyo, which are on flood plains and regularly used to get flooded (no climate change required, just regular rain season/typhoon does this). Now due to urban sprawl more people want to live there, exacerbating the problem and creating the need for this system.
I do not doubt that climate change is happening. I just don't like articles with such a clear agenda in the background, especially when the official sources contradict the statements.
[1] http://www.ktr.mlit.go.jp/edogawa/gaikaku/intro/01intro/inde...
(Please correct me if I'm wrong or I missed something.)
FWIW, the source code looks fairly solid to me, considering that it's a bash script meant to be used on trusted inputs.
To illustrate my point, look at the elaborate loop to iterate over *.gpg files: https://git.zx2c4.com/password-store/tree/src/password-store...
This looks to me like the correct way to do this in bash, as long as you can guarantee that $PREFIX does not start with whitespace (which may be a valid assumption here).
From what I can tell, the code quality is way better than what you see in your average bash script.
The easiest way is still: for file in *; do ...; done
This works fine with spaces and other strange characters, no need to come up with more complicated ways.
If you must use find, the correct way is really tricky and uses obscure bash features like settings IFS to the empty string to split on null bytes and process substitution so that the loop doesn't run in a subshell (which would prevent it from modifying variables in the current environment):
while IFS= read -r -d '' file; do ... done < <(find /tmp -type f -print0)
for file in *; do { ... }; done
is both much easier and much safer than piping the output of ls.
It does the correct thing with filenames containing spaces or weird characters, and the intent is much more visible, so there is really no reason to use $(ls).
More details: http://mywiki.wooledge.org/ParsingLs
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.
These articles don't say that regular tubes are faster than transistors, only that "vacuum-channel transistors" (nano-scale devices inspired by tubes but different) could possibly eventually be faster than semiconductors.
But these articles are from 2014 and 2012 and they contradict easily looked up facts. The 2012 article claims that this technology promises speeds of up to 460GHz, which seems to have already been topped by regular semiconductor transistors, even by 2003: See https://en.wikipedia.org/wiki/Milton_Feng#World.27s_fastest_... for a really old example.
So to me it seems that this research is in a very early stage and no one knows whether the finished product (if it is ever finished) will be faster than semiconductors. Of course the researchers working on this must make big promises or they wouldn't get grants, but that's how the grant system works today, and it doesn't tell you anything about how viable the product is.
edit: Not to sound to negative here, I am really looking forward to this new technology and hope it will turn out alright. But it looks very much like fundamental research, so I take issue with broad claims like "by their nature, tubes are much faster than semiconductors, which has its uses", when apparently nothing has left the laboratory yet.
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.
Another downside of the FireTV stick and a dealbreaker to me is that Android cannot adapt the refresh rate to the frame rate of the video. Many movies are 24fps, so a multiple of 24Hz is required on the HDMI port for smooth playback. It's one of those things you can't unsee once you're aware of it.
Maybe they've fixed it, but it was like this half a year ago when I had a FireTV stick.
The site offers https but is broken when using it. It shows no questions.
The fact that character ranges like [a-z] can depend on the value of LC_COLLATE is also something not many people are aware of.
$ echo "ä" | LC_COLLATE=C grep '[a-z]'
$ echo "ä" | LC_COLLATE=en_US.UTF-8 grep '[a-z]'
ä