Hacker Newsnew | past | comments | ask | show | jobs | submit | philipfweiss's commentslogin

I haven't seen this publicized widely, but it's really good content that flies under the radar. Posting here in case people find interesting.


Type theory is actually a stronger axiomatic system than ZFC, and is equiconsistent with ZFC+ a stronger condition.

See this mathoverflow response here https://mathoverflow.net/a/437200/477593


To echo the sibling comment, that answer is specifically referring to the type theory behind Lean (which I’ve heard is pretty weird in a lot of ways, albeit usually in service of usability). Many type theories are weaker than ZFC, or even ZF, at least if I correctly skimmed https://proofassistants.stackexchange.com/a/1210/7.


You’re not doing calculus on a graph- you’re using a graph algorithm to automate the derivative taking process.

Essentially, you transform your function into a “circuit” or just a graph with edge labels according to the relationship between parts of the expression. The circuit has the nice property that there is an algorithm you can run on it, with very simple rules, which gets you the derivative of the function used to create that circuit.

So taking the derivative becomes:

1. Transform function F into circuit C. 2. Run compute_gradiant(c) to get the gradient of F.

Lots of useful examples here: https://cs231n.github.io/optimization-2/


That is a great example. It's rarely bad to be pedantic if it leads to better understanding!


The rationale I remember learning was:

Think about your blood vessels. They run, and branch, and then branch again, in an intricate pattern. Your DNA has to encode for this, but our DNA holds a finite amount of information.

So does it seem more likely that your DNA holds bit of information for every branch of every blood vessel? Or instead, does it just encode the information of “blood vessel branches half way into a new blood vessel, recursively”. The fractal can be encoded with fewer bits, as the instructions to make the original vessel can be repeated at the split point.

It’s kind of like… you don’t store information of all humans in your lineage. Rather, you store information for one human, as well as information for how to make copies.


What if... the author wasn't aiming this post for a completely lay audience, but rather someone with a undergraduate/graduate level of mathematics/physics background who was interested in learning more about some phenomenon?


Nope everything needs to be completely intuitive, explaining in detail is completely wrong /s

I think both can complement each other, but it is definitely nice to go into the details. Watch the Feynman explanation then try to use that as you go through the actual details. The initial more hand wavy, but morally correct explanation, gives you something to latch onto, and then you can use that to guide your reasoning in the more complicated steps.

Honestly the idea or expectation that things need to be read linearly is also wrong, you should include some reasonable level of detail and elaboration in your writing, but organise it so it can be picked over. You can switch betweeen levels too.


Qiaochu, unrelated, but I really enjoy your contribution to MathOverflow. This article is equally solid :)


I played a game of codenames, where I was the only guy on a team. I had an awesome clue- Flashbang: 4.

None of the women on my team knew what it meant. Every guy in the room did. We lost the game, but it was a very interesting social experiment.


Love that story. Makes me think playing Codenames in German, where all kinds of words are made by mashing other words together, would be a great advantage over playing in English.


Well, this rather makes the game annoying to play with people who think they are so clever and start constructing completely new words no one before them ever used. Which the rules don’t allow, by the way.

Sure, you can construct arbitrary new words in German. That works. However, that is certainly not the spirit of the game. Which the game does make abundantly clear in a quite long section of the rules. (I just got the game and its rules from our board game shelves, used the new OCR feature in iOS to copy and paste the relevant text into DeepL, cleaned up the translation and am now pasting it here with my own annotations in brackets. That was a cool experience.)

Excerpt from the rules:

Compound words

German is notorious worldwide for its compound words. There are two ways to form such in German. „Tischdecke” (tablecloth) is one word. „Mehrzweck-Fräsvorsatz“ (multi purpose milling fixture) is in principle also a word, because the hyphen merely serves to make it easier to read. „Rindfleischetikettierungsüberwachungsaufgabenübertragungsgesetz“ (beef labeling monitoring tasks transfer law) actually used to be a real (and awful) word, which probably would have been a little easier to read with a few hyphens. (We won't discuss the bad habit of breaking up compound words in German with – incorrect – spaces here). Strictly speaking, then, all such words can be valid clues, but only if they correspond to actual usage. It is easy in German to simply invent composites: „Tentakeltrabant“ (tentacle satellite) would theoretically be a great clue for „Oktopus” (octopus), „Mond“ (moon), and „Auto“ (car, because of the East German car „Trabant”), for example, but since it's only a word creation that you can't find in any dictionary, you can't use it.

Prefixes

This actually belongs to the previous rule, but should be mentioned explicitly: Simply turning a word into its opposite by putting a syllable like „kein-“, „nicht-“ or „un-“ (non-, un-) in front of it should only be allowed if this word is colloquially used. „Unlebendig“ (unalive) is therefore not a permitted clue for „Tod“ (death), „untot“ (undead) on the other hand would be permitted as a clue for „Skelett“ (skeleton).


My favourite compound German word is Fledermausmann aka Batman.

With the literal English translation of flying mouse man.


“Fledern” is not actually a German word (in any kind of common usage at least). A literal translation of flying would be “fliegen”.

Apparently the word fledermaus originates 1200 years ago and is derived from “flattern” (to flutter).


"Fluttermouse-man" is even better.


Love this


When playing codenames in German you usually have the dictionary rule / Google rule.

If you come up with a word and you aren't sure if it exists check if it is in the dictionary or if Google knows it.

So no making up words like

Mixerversicherungsfahrzeug


For the less masculine (or clued-in) members of the audience, what was the code word? Something to do with shooting games?


Probably "grenade". A flashbang grenade is a bright and loud but less destructive grenade used to startle people before an attack. Widely used by American police investigating possession of trivial amounts of marijuana.


In that game, the number said after the clue tells you how many of the words in play are related to the clue. So the word flashbang wouldn't be hinting at a codeword, but four of them.

So it could really be anything, e.g. bang, army, light and blind.


Since it's codenames, I would guess some of the words on the board they were hinting at would be WW2/war/call of duty/video games related stuff like France, Ear, Lag, Light, Hand, Hurt, Mud, Radio...


Something police use to disorient and theoretically help disperse a crowd - like a grenade except it creates only a mostly-harmless noise and flash of light.


> mostly-harmless noise and flash of light

Not that harmless. They don't throw fragmentation shrapnel but they are strong enough to punch holes into people when in direct vicinity. US police regularly throw these into cribs and kill or maim babies and toddlers.


Nelson is brilliant- i've enjoyed his blog tremendously over the years.

Especially his posts on how to properly think about testing. - https://blog.nelhage.com/post/testing-and-feedback-loops/


Was watching this lecture, and was startled to hear the Dan Boneh mention that P-256 might have a backdoor.

Gist: the seed for the curve has unknown origin. Possible attack: let's say there is an attack possible on 1/10^6 curves. Just loop through a million curves until you find one vulnerable, and publish it into the standard.


Note: I'm not affiliated with this project, but I saw it recently and think it's really cool. It seems they're trying to do for collaboration / office tools what signal did for messaging. Pretty awesome.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: