@corbin@defcon.social

Corbin @corbin@defcon.social · Apr 05, 2026

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.

defcon.social

DEF CON Social

0

Corbin @corbin@defcon.social · Oct 16, 2025

"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.

www.evanmiller.org

Attention Is Off By One

Let’s fix these pesky Transformer outliers using Softmax One and QuietAttention.

0

Corbin @corbin@defcon.social · Oct 08, 2025

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.

1

0

Corbin @corbin@defcon.social · Aug 10, 2025

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.

0

Corbin @corbin@defcon.social · Jul 20, 2025

Copyright is the main reason that bandwidth is still expensive.

1

0

Corbin @corbin@defcon.social · Jul 05, 2025

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

#physics #science

defcon.social

DEF CON Social

1

0

Corbin @corbin@defcon.social · Aug 27, 2024

Replying to @nobody@mastodon.acm.org

@nobody@mastodon.acm.org @stargirl@hachyderm.io Sure. Those hints would be populated from a mapping either maintained via Cheeseshop or via local choices. Either way, there's politics going on; each individual mapping is a policy choice. In terms of Zooko's triangle, this would be the "centralized" option, which means that the import keyword would now functionally depend on whatever build/runtime configuration you've imagined. Not that this is a bad thing! Check out PEP 302 for the hooks you'd need to prototype an actual implementation of your idea. Allen Short explained how to use PEP 302 here https://web.archive.org/web/20180411011138/http://washort.twistedmatrix.com/2011/01/introducing-exocet.html and I used it to add hot-reload plugin functionality to a Python Minecraft server.

1

2

0

Corbin @corbin@defcon.social · Aug 27, 2024

Replying to @nobody@mastodon.acm.org

@nobody@mastodon.acm.org @stargirl@hachyderm.io I'll note that this suffers from Zooko's triangle, a trilemma in nominal logic: https://en.wikipedia.org/wiki/Zooko%27s_triangle Imagine every Python module were content-addressed somehow, and packages too. This only kicks the can down the road, because you'd probably rather import from a petname than from a SHA-256 hash, so somebody must now set up a petname-to-hash map, and all of the existing political issues of the Cheeseshop reappear upon the maintenance of that map. (This is why politics is an inevitable part of maintaining large ports trees too.)

0

8

0

Corbin @corbin@defcon.social · Aug 27, 2024

Replying to @nobody@mastodon.acm.org

@nobody@mastodon.acm.org @whack@hachyderm.io @stargirl@hachyderm.io It's a fair critique, though, and one that spawns from the *same* memetic issue as in Python packaging, so it's worth examining. Sure, a Nix package *should* only rely on being located in /nix/store next to its dependencies. But as you've listed, there's piles of ambient authorities and mutable state which also must be correctly configured in order for some packages to run. This is *exactly* analogous to Python packages which aren't pure statically-imported Python modules. In a simpler world, we would deploy Python apps by tossing all Python modules into a single ZIP file, but because CPython allows extension modules and exposes a C API, a practical Python app must also depend on C runtime and C linkage. This isn't hypothetical. RPython, the toolkit for building PyPy, is pure Python 2.7. My rpypkgs flake https://github.com/rpypkgs/rpypkgs "installs" RPython packages by unpacking all of them to a common build directory.

1

0

Corbin @corbin@defcon.social · Jun 22, 2023

Replying to @cr@sigmoid.social

@cr@sigmoid.social @emilymbender@dair-community.social I didn't know that Tegmark was a practicing software engineer. I don't doubt that he can read and comprehend the literature, and I know he's listed as a co-author on several papers, but I think it's important to credit the actual hackers who do the work. In the case of Tegmark's recent ML publications, this appears to be https://github.com/ejmichaud and https://github.com/KindXiaoming who are Tegmark's graduate students. To Tegmark's credit, he gives them the primary authorship on the papers I skimmed. This is a non-trivial nuance: folks who don't multiply the matrices seem to have a distinct epistemology for large models, and this will color their ability to estimate the state of the field and probability of doom.

1

0

Corbin @corbin@defcon.social · Jun 22, 2023

Replying to @emilymbender@dair-community.social

@emilymbender@dair-community.social The reporting uses "AI specialist" as a label for clowns (Yud, Bostrom) and non-technical folk (Altman, Tegmark) as well as y'all at DAIR and other reputable organizations. This is better than typical IEEE fare but still not fair to actual practitioners.

1

2

0

Corbin @corbin@defcon.social · Jan 18, 2023

Replying to @whack@hachyderm.io

@whack@hachyderm.io @stargirl@hachyderm.io Sure; along with NixOS, the container environment ("FROM nixos/nix") and Darwin are better-supported than classic LSB distros. Aside from #X11 and other system services, Nix is self-contained; however, Nix is not the goal, but part of the journey towards package-capability security.

0

Corbin @corbin@defcon.social · Jan 16, 2023

Replying to @stargirl@hachyderm.io

@stargirl@hachyderm.io #Nix offers a genuine solution and a path towards packages as capabilities. #nixpkgs has a mature #Python subsystem. No involvement with PSF is required.

8

6

0

Corbin

Posts

DEF CON Social

Attention Is Off By One

DEF CON Social

Remote instance