This seems better to me because "getting around to more different things" is parallelizable, whereas "having K-x more serial time" is more general/powerful and you'd probably want to use it in a better way than that. (Though there's probably also a better way to use clones than "getting around to more different things").
Recent events have updated me towards thinking that a decent fraction of Americans (10-40%?) will rationalize and go along with ~anything the current admin does. My more general takeaway is that worryingly many humans are cognitively set up to fall for an authoritarian even in a modern western cultural context.
I'm also getting worried that the current admin expects to succeed at ending free elections, given how they keep doubling down on stuff that seems like it will play terribly with a majority of voters.
(Edited from a comment I wrote just now)
Recent events have updated me towards thinking that a decent fraction of Americans (10-40%?) will rationalize and go along with ~anything the current admin does. To me this doesn't seem to have all that much do with the "culture war" as I took the phrase to mean, but rather that worryingly many humans are cognitively set up to fall for an authoritarian even in a modern western cultural context. I agree that we need to figure out how to live with them.
I'm also getting worried that the current admin expects to succeed at ending free elections, given how they keep doubling down on stuff that seems like it will play terribly with a majority of voters.
1LW feature request/idea: something like Quick Takes, but for questions (Quick Questions?). I often want to ask a quick question or for suggestions/recommendations on something, and it feels more likely I'd get a response if it showed up in a Quick Takes like feed rather than as an ordinary post like Questions currently do.
It doesn't feel very right to me to post such questions as Quick Takes, since they aren't "takes". (I also tried this once, and it got downvoted and no responses.)
I'm looking for recommendations for frameworks/tools/setups that could facilitate machine checked math manipulations.
More details:
- My current use case is to show that an optimized reshuffling of a big matrix computation is equivalent to the original unoptimized expression
- Need to be able to index submatrices of an arbitrary sized matrices
- I tried doing the manipulations with some CASes (SymPy and Mathematica), which didn't work at all
- IIUC the main reason they didn't work is that they couldn't handle the indexing thing
- I have very little experience with proof assistants, and am not willing/able to put the effort into becoming fluent with them
- The equivalence proof doesn't need to be a readable by me if e.g. an AI can cook up a complicated equivalence proof
- So long as I can trust that it didn't cheat e.g. by sneaking in extra assumptions
I agree with this critique; I think washing machines belong on the "light bulbs and computers" side of the analogy. The analogy has the form:
"germline engineering for common diseases and important traits" : "gene therapy for a rare disease" :: "widespread, transformation uses of electricity" : x
So x should be some very expensive, niche use of electricity that provides a very large benefit to its tiny user base (and doesn't arguably indirectly lead to large future benefits, e.g. via scientific discovery for a niche scientific instrument).
I think you're mixing up max with argmax?
Something I didn't realize until now: P = NP would imply that finding the argmax of arbitrary polynomial time (P-time) functions could be done in P-time.
Proof sketch
Suppose you have some polynomial time function f: N -> Q. Since f is P-time, if we feed it an n-bit input x it will output a y with at most max_output_bits(n) bits as output, where max_output_bits(n) is at most polynomial in n. Denote y_max and y_min as the largest and smallest rational numbers encodable in max_output_bits(n) bits.
Now define check(x, y) := f(x) >= y, and argsat(y) := x such that check(x, y) else None. argsat(y) is in FNP, and thus runs in P-time if P = NP. Now we can find argmax(f(x)) by running a binary search over all values y in [y_min, y_max] on the function argsat(y). The binary search will call argsat(y) at most max_output_bits(n) times, and P x P = P.
I'd previously thought of argmax as necessarily exponential time, since something being an optimum is a global property of all evaluations of the function, rather than a local property of one evaluation.
TBC, by "going along with" I meant something like "explicitly approving of". Agree that the proportion that wouldn't directly try to do anything about it (besides voting) is much higher.