fspeech

62 ms·

691.
by fspeech 7y ago
Poisson distribution is the limit of having infinite particles around.
692.
by fspeech 7y ago
It would be nice to have some of the proof checker instrumentation for fast starts upstreamed into HolLight.
693.
by fspeech 8y ago
Once you have the job a master's degree is a master's degree. If your employer (esp. large ones) has some benefits in place for possessing a master's you will qualify. However when you apply for jobs hiring managers may not k
694.
by fspeech 8y ago
Thanks for the link. Watching it I can't help but feel a little sad. Prof. Stein is a highly trained mathematician with a track record in establishing successful software projects like Sage that many people benefit tremendously from (w
695.
by fspeech 8y ago
Here is the reuse record so far: https://www.reddit.com/r/spacex/wiki/cores
696.
by fspeech 8y ago
For dense urban areas land cost could exceed building cost. However for ghost cities land cost (defined as an opportunity cost) is low to begin with. While building material may have alternative use, if the labor used to build buildings don
697.
by fspeech 8y ago
I think he was talking about angular resolution. EM wave arrives at different antennas at slightly different time. The phase difference allows for very high resolution of the direction the wave is coming from. [VLBI]( https://en.m
698.
Spinning Water Droplets That Seemingly Defy Physics(nytimes.com)
4 points by fspeech 8y ago|1 comments
699.
by fspeech 8y ago
Hol is in sml. HolLight is OCaml.
700.
by fspeech 8y ago
For people not familiar with the subject (or Buzzard and his cohort) I recommend checking out the Zulip archive https://leanprover-community.github.io/archive/116395maths/i... Some of the (esp. earlier) threads ar
701.
by fspeech 8y ago
You can be as abstract or concrete as you want. For example you can embed set theory inside a category (see Lawvere, Rosebrugh: Sets for Mathematics or https://ncatlab.org/nlab/show/ETCS ). The main thing is that y
702.
by fspeech 8y ago
I thought Dedukti has a small kernel. Although “small” may be a relative thing (relative to other dependently typed systems.
703.
by fspeech 8y ago
I was wondering about termination. With finite ground facts that appears not to be an issue. Complexity is another matter.
704.
by fspeech 8y ago
Can you specify symmetric and transitive closure in Datalog?
705.
by fspeech 8y ago
Which is why they need a network of the grids like the local ones in existence today. If you have 10 lines feeding into a mega city from different directions the reserve for a single failure can be lowered to 10%. You can also build pumped
706.
by fspeech 8y ago
Read "How Huawei tried to sell itself to Motorola for $7.5bn" which was published by FT four days ago. The deal was advised by JP Morgan and Morgan Stanley. It fell through at the final stage due to leadership change at Motorola.
707.
by fspeech 8y ago
Alloy (and the philosophy it is based on) is explained in Daniel Jackson's book <<Software Abstractions>>, which is a very nice book to read on techniques of specification and verification (at the specification level).
708.
by fspeech 8y ago
Prolog is a general programming language with built-in backchaining semantics. It in general does not know how to solve constraints. Indeed if your clauses have loops Prolog will just run in circles until it is out of stack space. The follo
709.
by fspeech 8y ago
One has to look at the policy details. At 7 percent + CPI it is not going to create abandoned properties over the long term. It is more like preventing Uber style surge pricing. There is a reason why the association for the landlords are ne
710.
by fspeech 8y ago
"Otherwise it can just buy them itself to keep interest rates in check." That would be no difference from "redeeming". Bond prices are determined by interest rates. When interest rate is the same as coupon rate the sell
711.
by fspeech 8y ago
“It's just impossible to write a general-purpose algorithm to solve it in all cases.” That is the definition of an undecidable problem. Independence, as in Euclid’s fifth postulate, is not what we typically think of as undecidability,
712.
by fspeech 8y ago
This is the first paragraph from the Wikipedia article on undecidable problems: “In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct
713.
by fspeech 8y ago
Undecidable means there is no logical way to have an answer. Turing’s halting problem is one such.
714.
Chinese open source platform(gitee.com)
2 points by fspeech 8y ago|0 comments
715.
by fspeech 8y ago
This reads like an faq for people coming to US. First item reminds people to buy travel/health insurance. Second item warns against going out alone in late night. Etc. I didn't see anything political in it.
716.
by fspeech 8y ago
For me Cython truly shines when interfacing to C++.
717.
by fspeech 8y ago
The balance is between Moon and Earth gravity. However it is more subtle than that at L2 as both gravitational forces are in the same direction so they don't apparently cancel. The way to see it is to realize that L2 is relatively stat
718.
by fspeech 8y ago
My younger son (high school freshman) would agree. He informed me that it is very addictive. Some kids try it out of curiosity and then become very addicted. It is easy to hide at school. He calls their bathroom the vape lounge. Kids can va
719.
by fspeech 8y ago
If you look at the graph I provided and zoom out to the 5 year chart, you would see a fairly large drop in Chinese imports around 2015-16. Part of that might have been due to commodity price drops, but I suspect the correlation of US export
720.
by fspeech 8y ago
Chinese import growth over 2018 was mostly in the double digit range (averaged 14.6% Jan. through Nov.). Its imports from Europe, Japan and ASEAN grew 10% or higher. https://www.ceicdata.com/en/indicator/china&#x2F

More ›