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.
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.
Of course you can't ignore details. I was explaining the source of emotions, which tend to drive whether one wants to adopt a particular tool or method.
That being said, I often find convincing, false proofs as illuminating as true proofs, once the flaw is clear, because they highlight the nature of the conjecture. So I disagree with your claim that a proof can suddenly become useless due to a slight misstep.
And for what it's worth, theorems are rarely thrown out due to pathological corner cases; at least I've never heard of this happening. Instead, if the insight conveyed by the proof is useful, it's called a partial result and the conditions are modified to fit the proof. Entire theories are built up specifically to avoid pathology (almost every mathematical field does this)
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.
Also too, of course you should build your "prevent floods from wrecking our shit" system to handle floods "beyond anything we've seen before". Building it to handle less than what you've seen before would be stupid.
> Building it to handle less than what you've seen before would be stupid.
Let me tell a second hand anecdote of a Burmese village.
It was a rather small collection of huts raised on tall poles. But it was a village none the less.
All paths in the village were laid out with a connected mass of wood. Along the path were sticks, rising pretty high up in the air. Somewhere along the top of the sticks were a lot of cuts made out in the wood, at various heights. By a knife or so.
In the dry season, this path laid on the ground to be walked on. You didn't have to walk on it of course, since the surrounding dirt was dry.
In the wet season however, floods often came. And so, they raised the path up along the sticks so that it became a water bridge for when floods came. They raised it to the level of the highest cuts that were made in the sticks. A very reasonable thing to do, in order to connect the village in times of crisis, without using boats.
Interestingly, however was the background of the cuts. Each cut represented a water height that had some time ago been the highest the flood had become. So each season, they only raised the water bridge to the level of the worst flood they had experienced.
They did not have a margin.
While they didn't prepare for less than what they had previously seen, they only prepared for the worst flood in history, and not the worst flood in history + a margin.
Did they have room on the uprights to tie the cross members higher? Maybe the flood water held the wood up (buoyancy) and the uprights were there as anchors.
How did they raise the wood? I imagine it weighed a lot.
That isn't entirely true. How much is it worth to upgrade from a "once every 500 years" system to a "once every 5000 years" system? If it's more than the expected damages...
When you start talking truly cataclysmic events, the value of the physical infrastructure at risk will be dwarfed by the human lives. In 2016, the assessed value of all real estate in Manhattan crossed the $1 trillion threshold (which of course leaves out the bridges, the subways, the personal property...) At a value of $9.1 million / life, there are $77.7 trillion worth of humans in New York City.
If there's a natural disaster which would wipe out the population of New York once every 5000 years, we should be willing to spend $15 billion per year to prevent it.
Because the reason is building codes, cutting green areas.
Flooding is almost always related to changes upriver.
Storms and climate change related water level rises are a danger, but not the main reason.
Isn't it an agenda to call the consensus reality an "agenda"? I'm not being facetious, but that discourse has fallen the point where simple statements of reality are politicized has dumbed the entire discourse.
I can only speak for myself, but analogously, I have no disagreement when the anti-vaccination contingent paints the rest of us as having an "agenda" when we post stories about horrible flu outbreaks. Herd immunity and total extinction of certain viruses are definitely an "agenda" I will own up to supporting.
Calling it a consensus reality is also showing an agenda - trying to make it sound more certain than it is, which is to push the agenda of saving people from possible harm of future climate change by fooling them into believing it's certain because they're not competent enough to assess the risk of uncertain things. I'm not complaining about trying to do good, but it's not science, it's belief and it might be wrong.
The rest of science doesn't get described so confidently because people don't care if the general public believes it or not. If you're interested in understanding, not politicizing, then it doesn't matter if there's a consensus or not. Look at the history of consensuses about how nature works to see how unhelpful they are at determining what reality is.
> The rest of science doesn't get described so confidently
Um what? I feel like you haven't spent 10 minutes in a physics class. As someone who spent many years studying physics, you have to get within range of the quantum level before people in that field start feeling a little shaky in their beliefs.
The history of consensuses? Yes, please, you should do that, because it has gotten us quite far given the constraints of time. There are so many crackpot ideas that are thankfully rarely explored due to consensus.
Things that were described confidently for centuries (or less):
1. The earth is flat.
2. The sun revolves around the earth.
3. Fire is an element.
4. They have chemical/nuclear weapons.
5. No one can enter the search market; AltaVista owns the market.
6. Pets.com can't fail - look at who is invested and how big is the market.
7. Noone will ever need more than 640K of ram.
8. There is a world market for maybe 5 computers.
etc. Who cares how solid the consensus is - what matters is facts and truth.
Congrats. You poked a hole in the meta-consensus, proving the point.
You ignore the others, that dogma leads to shallow thinking.
All the world is the blend of chaos and order; acceptance and rejection, yin and yang. Your contribution helps drive the analytical consideration of acceptance or rejection.
I accept that dogma can allow wrong thoughts to persist, to drive criticism underground.
I accept that prevailing scientific/expert opinions can also be right.
I accept that the claim of climate change, if true, would have disastrous consequences on a huge number of human lives, and of course business.
I also accept that I'm not seeing people studying this field denying human caused climate change.
I am not seeing countries other that the U.S, where it has become political, denying climate change.
In fact, I see a larger number of nations in the world agree on something than ANYTHING in human history. These countries have their own scientists.
I can certainly entertain that a few countries might make false claims to push other countries to make bad investments. But you're claiming that a global conspiracy on a literally unprecedented scale is happening and that we should ignore a high consequence concept because a relatively small number of people that happen to come from the single country where it is a political issue and to a dizzying degree come from outside the field say everyone else is wrong?
I'm not a climate scientist. I've done a little digging and have my own guess as to what is likely correct, but frankly my opinion of this is low confidence because I'm so ignorant on the topic. When one side says volcanoes are orders of magnitude less greenhouse gas contributers than humanity, and the other side says the reverse, any decision I make is based other than evidence.
Using the same criteria I use to decide what OTHER scientific advice I follow, I conclude that there is a chance that counter positions to climate change are correct...but is more likely that they are wrong.
High chance of occurrence x high consequence if it happens = you need a lot more evidence than I've seen.
If the history books in 500 years talk about how humanity put forth a lot of effort to stop a calamity at a global scale that turned out to be snake oil, that is still a result preferable than about how people followed dogma that lead them to discount repeated evidence and the millions or billions of people suffered for generations. That might sound like a straw man - i could say that failing to rub my head daily would have disastrous consequences - but when paired with the likelihood that someone on the internet saw through this global hoax, it is part of my reasoning.
May I ask your profession and country of residence?
"But you're claiming that a global conspiracy on a literally unprecedented scale is happening"
No I'm not actually. What I'm saying is what I said. It was in reference to the ancestral post asserting that arbitrary confidence was being applied to certain statements.
Scientists were widely confident about the correctness of Newton's 2nd law and the universal law of gravitation up till the late 1800s/early 1900s. Then Einstein showed their limitations/incorrectness. You can't look at contemporary modern consensuses because if it's a consensus, it'll look like it's right until the future when/if it's proven wrong.
Philosophy of science says we can't prove theories (of a certain type, which includes most of physics), only disprove them. So there aren't scientific truths, just current best theories.
Many cultures had religious myths about the history of the world which they widely believed.
I'm not saying that people who disagree with the consensus are necessarily right, or even that we should bother to listen to them - just that sometimes they might be so consensus isn't a reason to judge something as true.
> Scientists were widely confident about the correctness of Newton's 2nd law and the universal law of gravitation up till the late 1800s/early 1900s. Then Einstein showed their limitations/incorrectness.
While Einstein revised them, the Newtonian equations are correct enough that they are still generally used for all kinds of things.
If that the best example you can use to make the argument that the current scientific consensus could be wide off the mark, you've done more to refute your argument than advance it.
Bloodletting. It's honestly trivial to find examples of where science was wrong. I'm not going to research them for you if you'll make up ad-hoc reasons to reject them.
Obviously I can't give an example of current consensus being likely wrong because if I knew that, scientists would too and it wouldn't be the consensus.
Here's a snarky example though. See if you can find the flaw in it - current consensus among scientists is that you can't prove causation without doing an experiment - in particular you can't prove it using historical data. This is an obstacle to medical research since ethics impedes controlled experiments on people and it's part of why nutrition advice is frequently wrong (there you go for even more examples). But climate scientists have apparently done just that - themselves demonstrating that either the consensus is wrong or they're wrong. Either way, a consensus is wrong.
These are just an arguments to show how wrong consensus can be though - in reality I'm pretty sure that climate scientists don't acutally believe they're right without any doubt. It will be politics and attempts to manipulate people that changes confidence values into supposed certainty.
Cannot prove causation is not the same as cannot conclude causation. As you point out with your medical example, we have plenty of cases where we act with evidence but not proof. Sometimes these are wrong...but more often they are not (when talking about science).
Often there is some evidence in both directions (for/against a theory), so we likewise have experience and examples where we must decide based on that imperfect info.
Given that we will never be able to prove this causation, at least not in the next few lifetimes and given that, right or wrong, the people (vast majority) in the field are saying the problem is real; Given that inaction is terrible if this is all true, then what evidence would convince you (or any example climate change denier) that the concerns are valid?
My problem here isn't that I think the concerns aren't valid, but that whenever the topic comes up, multiple people start to push the agenda of "we must all take action now", as if they're trying to drum up an army of supporters, which they probably are. It gets embedded in just about any climate change related discussion, news article and even science paper.
You can't even disagree with anything related to the topic without people jumping to the conclusion that you're a climate change denier and insisting on educating you. It shuts down genuine discussion. Even evolutionist arguing creationists have managed to admit that it's just a theory, but then go on to show how strong theories can be which is perfectly righ. Climate change hasn't got to that level of honesty - people are afraid to say it's just a theory because of their agenda.
I can sympathize with your position - a lot of good discussion can't happen on various topics because you have to defend against the ridiculous.
Re: GMOs - you want to discuss the impact on monocultures, chemical levels and environment impacts (good or ill), prions or other corners of proteins we don't understand, patented genes, wild release of genes (including the patented ones), the economic value in talking cost vs improved yield, or even a serious discussion about what level of labeling (if any) is reasonable? Too bad, you're going to have to deal with people that think GMO food will mutate THEM if eaten.
climate, gun control, vaccines, free speech, etc - you can't have a nuanced, serious discussion to explore details because you have to fight off the fringe(s).
OTOH, however, a higher-than-linear curve of greenhouse gas emissions and year after year, into decade after decade of inaction, has an impact. The 2 degree threshold isn't a firm line...but it's also not arbitrary. If we need to make drastic change, but we've frittered away the decades that COULD have made that more gradual, then yeah, importance of action is higher. I'm not saying we have all stop driving tomorrow...but our current pace is not what we need, so the pressure is up. If we weren't taking as many steps backwards as we are taking forward, if the models said we were closer to a target than the projection said 10 years ago, that'd allow some reduction in the pressure. Instead of saying "we just need to keep our eye on the ball" we have to say "LOOK! THERE'S A FRICKING BALL!".
So I can understand the sense of urgency. Like race relations or gender issues in tech, any complaint that people are overreacting, or that this isn't the time, or this isn't the place has to come with some believable explanation of how they see a better way that hasn't been tried and failed.
To your concluding point: Climate change is a theory. I'll admit that. It could be wrong. The overwhelming majority of those in the world with relevant data and experience can be wrong. Really. But I don't see much evidence that that is more likely than the theory being mostly correct.
With that admission, where are we? Well, we've agreed to something that was already not in question. But for most it's NOT an agreement. We have to somehow convince people that their gut instinct is not a value that should even be considered when deciding things. And again, and again.
When exactly will we STOP agreeing that it's a theory and move on to what to do with it? Will another 10 years be enough? 20?
How uncertain should man-made global warming sound, in your opinion? You're speaking in gross generalities, perhaps getting some hard numbers. What I've read is that nearly 100% of publishing researchers in the area agree on it (high 90's).
More helpful than the percentage of scientists who think it's true (a bizarre metric in science) would be the confidence they place on that conclusion. It can't be exactly 100%. Showing causation is notoriously hard, especially when you can only look at historical data, and even more so when there's only one example (one case of humans causing global warming).
This figure gets trotted out all the time and it's tiresome because it is so unconvincing to anyone who is even a bit sceptical.
That's a bit like asking what percentage of Christian priests believe God exists. There's kind of a selection bias there.
More helpful are broader surveys including earth scientists, geologists, etc, which (as I recall, not having the source handy) come up much more conflicted, close to 50% disagreement on various critical questions.
There also the issue of what questions are asked. It's easy to ask, 'is the climate changing', get a near-unanimous response to this near-tautological statement, and declare victory. But that question has nothing to do with any real disagreements real people are having.
The actual questions at hand are much more delicate. First among them is the question of what question we should even be asking.
> More helpful are broader surveys including earth scientists, geologists, etc,
Wait...while i agree that the methodology that gives 97% suffers a selection bias, I don't agree with the above. I would not trust a survey of priests about the existance of God, but I'd prefer their thoughts on the existance of a particular book of the bible than a survey of choir members.
Science is huge and detailed. I'd not trust geologists over physicists about physics. I acknowledge that physicists are not 100% correct, but that doesn't make non-physicists suddenly more likely to be correct.
I can see your point if the claim is 97% of scientists, but the claim is about climate scientists, because they determine the consensus on the topic.
What method of saying whether or not there is a consensus would you accept that doesn't involve bringing in people with no knowledge or experience with the topic?
You mentioned a 50%ish figure for scientists. Do you have a citation? Even if I think the result unconvincing (based on tjis limited info) I'd like to see their methodology and sample size.
His figure is probably based on a study specifically addressed in link I provided. Look for "Bray and von Storch (2007) and Bray (2010)" and the critique of their results and methodologies.
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)
I like that, I've never thought of or seen it, although it should've been intuitively obvious given how bash expansion works.
I think this demonstrates the point pretty well though - it takes a discussion among three of us before arriving at something that works moderately well, and we found four fairly different ways of doing it...
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).
I can't give you the source I got it from, as it is something I have read multiple times over the years from different sources. A quick search turns up a lot of articles on the subject, with the claim that centaur teams are better.[0]
I cannot follow you on the unintuitive part. If you have a chess program playing against itself, as long as it isn't capable of playing a perfect game every time, the program being supervised by a human should better, as the human will have a non-zero chance of spotting a mistake (or a better move) with enough plays. With low of the risk of mistakes from the weaker human, as she can confer with the judgement of the program. If the risk of human error is lower than the chance of human insight, the centaur team should have the edge on the lone computer.
After checking up on the subject again, it seems like the effect is no longer strong enough to topple the best chess computers though.[1]
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.
There are centaur championships in chess, for example ICCF. Mainly, people try do strategy and choose directions (which engines are not that good at) , while computer does the calculations.
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.
I want to emphasize an important distinction: that vacuum-based amps have higher potential switching speeds than semiconductors is not a novel thing, nor is it early stage research. It is part and parcel of the nature of semiconductors. What is cutting-edge is miniaturization of vacuum-based systems using conventional fab processes. That's the exciting stuff!
Depending on what you mean by "faster", there are applications when high power output is required at high frequency where tubes still win. Klystron tubes are an example:
https://en.m.wikipedia.org/wiki/Klystron
They are faster when high power is as much a requirement as high speed/frequency. Hence klystrons, magnetrons, thyratrons, krytrons, are still all used in that space.
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...