mbid

13 ms·

61.
by mbid 9y ago
EDIT: What follows is true for extensional MLTT. If you add univalence to intensional MLTT, all of this goes out the window. It is conjectured that you can replace "locally cartesian closed category" with "locally cartesian
62.
by mbid 9y ago
It is misleading to say that elementary toposes/zfc don't have something like identity types. Every elementary topos is locally cartesian closed, and locally cartesian closed categories are (equivalent to) models of extensional Ma
63.
by mbid 9y ago
You send a truncated digest of the password, which was obtained using a somewhat dubious hash function. I guess there are currently no known preimage attacks on this scheme, but revealing this information is more than nothing.
64.
by mbid 9y ago
And do they get the adderall prescription there? What does your friend's employer think about this?
65.
by mbid 9y ago
Yes, I know. It's certainly better to leak only the first eigth of your password than all of it, but it's still not something you should do.
66.
by mbid 9y ago
If you're already using a password manager, shouldn't you be using different (random) passwords for every service anyway? What's the point then? I guess it makes sense to use this if you've begun using a password manager
67.
by mbid 9y ago
Honest question: How many plastic straws do you have to save to offset the CO2 cost of building a steel straw? Also, are paper straws really better, CO2-wise?
68.
by mbid 9y ago
Every category is an infinity category, but the converse is not true. Thus, infinity categories are more general than categories. But you don't have to go that far: Just remove e.g. identity morphisms from categories, and you get somet
69.
by mbid 9y ago
There are serious efforts to found maths on elementary toposes, which are categories with certain properties. Much the same way that the axioms of ZFC model the properties of sets in terms of the "is element" relation, you can giv
70.
by mbid 9y ago
Right, but look at its dependencies. Arch links haskell packages dynamically, so you easily end up in DLL hell.
71.
by mbid 9y ago
I don't get it. Say I already know that I'll need some formulae in my document. Then the use case here seems to be, essentially, that I can write # Section Name instead of \section{Section Name} and that I can wr
72.
by mbid 9y ago
According to https://www.fs.lmu.de/angebot , this server hosts * a bunch of wordpress pages * mailing lists * mail server for council adresses, likely mostly unused * git server for a few student councils at LMU. Git is like
73.
by mbid 9y ago
> Its an n^2 problem > actually increases resource utilization exponentially I think you'll have to choose there.
74.
by mbid 9y ago
Not really what people/mathematicians would generally understand as "algebraic number theory". More like computational number theory or computational algebra.
75.
by mbid 9y ago
No, "willen" means "to want". The Dutch sentence is in present tense, your English translation isn't.
76.
by mbid 9y ago
And because google is the police of the internet, they had to do something about criminally slow webpages.
77.
by mbid 9y ago
Look at the source of motherfuckingwebsite.com. You'll find that it loads a certain analytics script. Motherfucker indeed.
78.
by mbid 9y ago
Thanks, but I think I've recovered from my curiosity.
79.
by mbid 9y ago
"Oh, the man would've died anyway some day, so I'm not really responsible for his death, I've only contributed."
80.
by mbid 9y ago
Hi Ingo, I'm pleasantly surprised to see an actual researcher here. For the most part, any two mathematicians working on different subjects won't believe that each other's work is relevant to them. This is somewhat true, bu
81.
by mbid 9y ago
Can't reply to everything here. I don't know to which extent Russel's type system influenced modern-day type systems in programming languages. Well no, they know sort of what they have to say. Yes, I agree. But I'd exp
82.
by mbid 9y ago
In 2013, a consortium of the greatest mathematicians published a massive volume which reboots our conception of mathematics. Ok, here's a rant by a frustrated student who's spent way too much time drinking the cool-aid. None of
83.
by mbid 9y ago
Actually you should look at the flip side of the coin: We - Germans - just decided that letting Nazis not speak their hurtful lies harms nothing of value. A majority deciding something doesn't make it just, as you as a fellow German
84.
by mbid 9y ago
Personnel counts grow at an exponential rate. Wrong usage of "exponential" seems to grow exponentially these days.
85.
by mbid 9y ago
There is no formal specification for what these algorithms are supposed to do, so you can't verify anything. Machine Learning isn't a mathematical discipline.
86.
by mbid 9y ago
As far as I can tell, the formal proofs themselves were always correct in his example. The problem was that the proved statements were not the ones intended.
87.
by mbid 9y ago
I don't quite understand why Z3 is part of the TCB. Isn't Z3 generally used to generate proofs which are then verified by the respective proof assistant?
88.
by mbid 9y ago
> My kids are netflix babies The times we live in...
89.
by mbid 9y ago
What are you talking about? Haskell is 30 years old.
90.
by mbid 9y ago
It's not obvious (and IMO somewhat doubtful) that it was the technical choices of the founders that made them successful. Their choices could well have been bad, just not bad enough to make their business fail.

More ›