Corbin

I've seen a couple blog posts floating around that talk about what "technical" means. Their discussions are good and interesting but don't directly get at the heart of the issue.

To be technical is to pay attention to details. That's all. A (classical) computer is a detail machine; it only operates upon bits, it only knows bits, and it only decides bits. To be technical is to try to keep pace with the computer and know details as precisely as it does.

Framed this way, it should be obvious that humans aren't technical and can't really be technical. This fundamental insecurity is the heart of priestly gatekeeping of computer science.

Copyright is the main reason that bandwidth is still expensive.

There's no evidence for determinism, let alone superdeterminism.

#physics #science

So, just double-checking how #Lean4 and #Mathlib work:

* Lean takes 3GiB of RAM and a minute to open Mathlib
* Lean requires about 10min to build itself in CI, only verifying required theorems
* Verifying all of Mathlib is measured in hours
* Lean's kernel is untrustworthy due to junk theorems

And yet I'm a clown for using #Metamath? At some point we ought to reconsider the type-theory fetish.

"Attention is off by one" (https://www.evanmiller.org/attention-is-off-by-one.html) led to attention sinks, which in turn led to better quantized models. But it appears that both Google and Meta independently discovered it internally, didn't fully document it, and didn't include it in their published papers; yet the code showed up in public contributions. In particular, it seems like PyTorch's version of multi-head attention has *never* been the version in "Attention is all you need", but always had functionality equivalent to what Miller describes.

There still is no moat. Attention sinks were independently rediscovered by the community upon doing some maths, and also the companies who discovered attention sinks internally did not prevent that knowledge from leaking out in implementation details. At most we might say that there is a time delay.

Memory allocation isn't required to have rich large values that are passed through control flow. Memory allocation is required for a stack and call/return semantics.