cvoss

38 ms·

451.
by cvoss 7y ago
Yeah, I would be surprised to see an actual Real Analysis course in an undergrad engineering curriculum. All of the Calculus courses, ODEs, and LA for sure. And these will lightly touch on all the topics listed on the real analysis Wikipedi
452.
by cvoss 7y ago
It seems like NSF is working towards that. NSF-funded publications must be publicly available for free within 12 months after publication. NSF has a repository for this purpose. This regulation went into effect in 2016. https://w
453.
by cvoss 7y ago
There's an important distinction (spectrum?) between automated theorem provers and proof assistants. Coq is a proof assistant, which means that any automation is there to try to help the programmer by clearing away the tedious parts an
454.
by cvoss 7y ago
Were you able to find this doc [0]? As best I understand it, a Prop P has as many inhabitants as there are proofs of P, whereas an SProp S has at most one inhabitant, according to whether it is true or not. All proofs of S are declared to b
455.
by cvoss 8y ago
In the usual setting, the various orientations of the centers are considered irrelevant because you can't tell them apart. So those points in the configuration space are considered the same point. There is such a thing as a cube with m
456.
by cvoss 8y ago
This is my hope and belief as well. Without the fire, much of it was going to have to be replaced/reconstructed at some point in the future anyway. It's an 850 year old building. In order to maintain it, we have to face the Ship
457.
by cvoss 8y ago
> "But with the rise of Protestantism, work was ennobled. Martin Luther for the first time suggested that an individual’s work—whether it was making shoes or building churches—could be a way of serving God, and that the harder we wo
458.
by cvoss 8y ago
Both kinds of pedal are typical, but it depends on the type of piano. For uprights, the una corda pedal moves the hammers closer to the strings so they don't accelerate for as long on their way in. But on a grand, the una corda pedal i
459.
by cvoss 8y ago
As others in the thread have pointed out, Euclidean geometry is decidable, but the proof of that fact corresponds to a highly inefficient algorithm for actually checking whether two points are equal. An alternative approach would be to &quo
460.
by cvoss 8y ago
The article goes on to explain just how wasteful our computers are, compared to the computations that go on in cells (which is a staggeringly large amount of computation, given their speed and abundance). > But the thermodynamic efficie
461.
by cvoss 8y ago
A word of caution: This textbook can get pretty bogged down sometimes because it serves double-duty as a Coq tutorial. (It has to, because the book is literally a Coq script, using formal theorems w/ proofs as examples and formal theor
462.
by cvoss 8y ago
The paradox in terms is entirely intentional. It is supposed to make you stop and think, "How can this be?", because it pushes back against many qualities often traditionally associated to leaders. So in fact, I stand corrected, a
463.
by cvoss 8y ago
I think (correct me if wrong) you have interpreted the phrase "servant leader" to mean "a leader of servants". Rather, it's intended meaning is "one who leads by being a servant".
464.
by cvoss 8y ago
This approach is still incorrect, and the bias toward the set of 4 points S = {(1,0),(-1,0),(0,1),(0,-1)} can be seen in the diagram. There is no way to break out of this bias by flipping or reordering coordinates because those two operatio
465.
by cvoss 8y ago
I didn't read the phrase "creation story" as literally referring the start of astronomy. It's a punchy allusion that fits well with the themes and thesis of the article.
466.
by cvoss 9y ago
A more precise, unit-respecting result is to plot the ratio of the unit sphere's volume to the unit cube's volume. This is a dimensionless quantity, so it makes sense to compare them, but happily the numeric values are unchanged b
467.
by cvoss 9y ago
I don't think he has. With his approach you would get results that are honest about their precision, like '3 plus-or-minus .0000000000000010'. That still doesn't help you decide whether or not the result is actually 3.
468.
by cvoss 9y ago
Ah, the legendary and beloved malloc lab. I am really glad they are working to keep this one visible and modernized. I know a lot of schools do this, but if you've never had to write your own allocator, I cannot recommend it enough as
469.
by cvoss 9y ago
The UI's prices were/are accurate as far as I can tell. I think the trading was just that unstable. When it opened at 17:20 PST, the price was indeed ~$3.5k, then shot up and down violently until they pulled the plug three minutes
470.
by cvoss 9y ago
(You may have omitted this detail on purpose, but I think it's worth pointing out) The example of trial division as a primality test is a good illustration of an algorithm that takes a lot of work to run but whose output is easy to ver
471.
by cvoss 9y ago
C/C++ is notoriously head-ache inducing on this point. Yes, all the CPU archs you'd reasonably expect to encounter today behave this way. However, because the language standard says signed overflow is undefined, compilers are free
472.
by cvoss 9y ago
Exponentially better than a polynomial in N is a polynomial in log N. See the abstract of [1] for the precise complexity claim about the algorithm mentioned in the article. As good as N^3 sounds, it's still not great on enormous system
473.
by cvoss 9y ago
There is a very direct sense in which pointer chasing _is_ the fundamental operation of sparse graph processing. On top of what access patterns the developers tend to use, there's always the JVM garbage collector (the bane of efficienc
474.
by cvoss 9y ago
A quick whois lookup suggests the domain name was registered on April 26. This is after we knew about EternalBlue and DoublePulsar, but suspiciously before the May 12th onslaught of WannaCry at the NHS. Also, the domain status is "serv
475.
Mysterious Microsoft patch killed 0days released by NSA-leaking Shadow Brokers(arstechnica.com)
4 points by cvoss 10y ago|0 comments
476.
by cvoss 10y ago
The game itself is certainly not the proof that is required. The proof in question is a proof that the game cannot be won by the adversary. By no means do you need to play all possible rounds of the game to conclude this.
477.
by cvoss 10y ago
> you didn't really prove every item gets counted in finite time The proof that the adversary cannot name such an item is logically the same as a proof that every item gets counted. This is a fundamental logical truth, namely de Mor
478.
by cvoss 10y ago
I find it helpful to think of countability in terms of the following game: You have a set of items in mind. You propose a (non-terminating) scheme for listing all the items in the set. An adversary attempts to name any item X, hoping your s
479.
by cvoss 10y ago
The article makes no mention of any proposed experiments. It sounds like the physicists are just using their understanding of the mathematics of quantum physics along with their intuition about such physical systems to guide the search for
480.
by cvoss 10y ago
Also we should keep in mind that it is currently spring break for Fulton, Cobb, DeKalb, and Gwinnett counties. Many families are out of town or have fewer activities to attend.

More ›