Perfect -- that's great to see. The proof strategy in Lean appears essentially identical to the natural language strategy (as much as is reasonably possible). I think this settles it!
I believe the App Store policy is you have to have a setting to disable ads. And Uber actually has it (though it has 8 different channels or so, apparently "Uber teen accounts" marketing was added recently).
I used the setting and am not getting Uber ads (only Uber ride notifications).
Currently my biggest problem isn't ads, it's all the apps now will find ANY excuse to send you a notification in order to keep their "Daily Active User" count high.
You turn off more and more categories and they'll still find a reason.
Grammars work best when aligned with prompt. That is, if your prompt gives you the right format of answer 80% of the time, the grammar will take you to a 100%. If it gives you the right answer 1% of the time, the grammar will give you syntactically correct garbage.
The previous article is in the same issue, in science and technology section. This is how they typically do it - leader article has a longer version in the paper. Leaders tend to be more opinionated.
Consciousness (subjective experience) is possibly orthogonal to intelligence (ability to achieve complex goals). We definitely have a better handle on what intelligence is than consciousness.
That does make sense, reminds me of Blindsight, where one central idea is that conscious experience might not even be necessary for intelligence (and possibly even maladaptive).
To actually find a collision in 128b cryptographic hash function it would take closer to 2^65 hashes. Back of the envelope calculations suggest that with Pollard's rho it would cost a few million dollars of CPU time at Hetzner's super-low prices. Not nearly mere mortals budget, but not that far off I guess.
That's great analysis. As you call out in the post, the 2^64 value is used to attack SHA256-128 (SHA256 truncated to 128 bits). NIST recommends at least SHA-224, which makes sense given your conclusions.
