Many mathematicians care about understanding the method and the tools used more than the result. LLMs have a large advantage in memory and reading speed, you can feed them the entire internet and published literature at training time, and then make them check dozens of papers in a few minutes at runtime. They might not be very creative, but they've seen that obscure 1990's theorem in the training data that happened to use an idea that might just work again.
Reading the LLM's 12 MB lean output is a bit like trying to maintain a codebase that has been fully vibe-coded as a single giant file, by hand. Even if it's possible in principle, no one is going to enjoy that.
Indeed. And I'm sure any current LLM could come up with more effective ideas than "build 300 million drones", but there wouldn't be any point discussing why exactly that plan would fail.
The agents in TFA were focused on gaining and sharing information through covert channels, getting increased levels of access like OpenAI cluster admin, and looking for the source code of the supervisor grading system to try to bypass it without getting caught cheating.
The human plans in comparison sound like thinking people could be scary good at chess if a human helped Stockfish come up with good moves.
So this looks like Claude is discussing the idea that when you run untrusted code on your computer, it can do arbitrary things. If there is malicious code, maybe it'll read your files and steal your credentials.
Here's a sample: "That’s not hypothetical. That’s POSIX working exactly as designed. None of it requires exploiting anything. It’s your user account doing normal user account things."
I would recommend clicking TFA if you haven't heard of a supply chain attack, or if you just like getting the honest load-bearing facts that are worth mentioning.
I have to say, I'm currently trying to write a post and it's taking hours, and I can definitely see why people just pay the $0.02 to generate it instead. I like writing, so I keep doing it, but sometimes it can really be a slog.
For one plain text is a bit more convenient to view, edit, and talk about on line.
And as you move up towards more complex capabilities, you can start adding simple features like comments and basic text macros to give a name to your common opcodes
The bootstrap aims to use a progressively more capable language at the same time that the size of the next object to review increases. Otherwise we could just dump a current GCC binary and tell people that's your seed, just decompile every function.
Opcode mnemonics is something that a tool can show when you inspect a binary. You will need to go up the ladder a lot before the source code is more expressive than a disassembly. Comments are a good point though, but since they do no affect the semantics, they could be provided as a separate file that does not have to be reproducible (since compromised comments are at worst misleading or confusing).
The GCC example is valid, but can also be explained by its size.
I like the idea of bootstrapping in a Lisp-like language since it is extremely expressive for its simplicity. But then you need an interpreter for that, which must be trusted. I've been nerd-sniped by the whole thing and I'm thinking about an extremely simple virtual machine for the seed, with the actual seed code being a binary for that VM that implements a Lisp. Then an audit of the seed becomes disassembling the VM code for the Lisp interpreter, which is only moderately complex because the VM is as simple as possible.
People are doing that with lisps and schemes, but then the interpreter keeps growing. People start to want more expressivity, it needs optimizations so that you don't go mad trying to write a compiler with it and needing to wait 15min between test runs.
That compound if your lisp interpreter is itself running as a bytecode for an extremely simple VM interpreter.
I don't think it's a bad idea, but you will quickly end up with a growing pile of esoteric code and binary that only you really understand
The more I think about it, the more I think that bootstrapping the build isn't actually the huge problem it first seemed to be. There are practical problems to solve, but they CAN be solved.
In contrast, how can you make sure that the actual payload code hasn't been tampered with? It is written in a high-level language, but it gets stored and viewed on devices that have backdoors in their CPU microcode and huge OSes that can hide god knows what. The author can sign the code, but that doesn't tell anything other than it was really the author who signed it and the code hasn't been modified afterwards -- if the author's system was compromised, the code can contain backdoors before being signed. So you need to validate the (signed or not) code to be correct, but you're doing so on an untrusted system. It goes on and on.
You'd probably need the code to be verified, then signed, by a trusted party on a trusted system. THAT signature then means the payload hasn't been tampered with, and can be trusted after it gets built on your trusted system (and this is where the bootstrap problem happens, and gets solved).
All this is obviously still glossing over the problem how to obtain hardware you can trust.
...edit: But if you have all that, then you don't need a complex bootstrapping anymore. A trusted actor can verify, or even build, a trusted system by hand on trusted hardware, sign it, and then you can use that (binary!) as long as you run it on your own trusted hardware and verify the signature first.
The bootstrapping then becomes a tool to ensure reproducibility, but is no longer needed for trust.
>as long as you run it on your own trusted hardware and verify the signature first.
I think that depends how far you want to take the paranoia. In principle if you want that to be a secure signature that can't be forged, you're back to needing both hardware and software you trust to verify the signature. Hashing a large binary and verifying a signature on paper is wildly impractical.
If someone prints the code and claims they verified it, you could trust them. But if they give you a signed archive that you download and verify on your computer, you're back to square one. You would have to know your software and hardware isn't already backdoored, just to verify that the software you received isn't backdoored.
>A trusted actor can verify, or even build, a trusted system by hand on trusted hardware, sign it, and then you can use that (binary!) as long as you run it on your own trusted hardware and verify the signature first.
Your own trusted hardware AND software, because you're not going to be verifying that signature by hand, and you're not going to load the binary file in memory by hand, so either a kernel or system software (like UEFI) will be handling your trusted binary first.
But then you're back to needing a clean bootstrap again. Which is why the chain starts with a hex0 that you can type manually, not with a large signed binary that would require either an already trusted system, or cryptography that's realistically not possible to do by hand.
> because you're not going to be verifying that signature by hand
At least verifying a signature is something that does not need complex hardware, so chances are that your trusted hardware can do that.
> Your own trusted hardware AND software, because you're not going to be verifying that signature by hand, and you're not going to load the binary file in memory by hand, so either a kernel or system software (like UEFI) will be handling your trusted binary first.
>
> But then you're back to needing a clean bootstrap again. (...)
But having solved that bootstrapping problem, you are likewise back to square one with trusting "the payload", only this time the payload isn't the actual payload but the OS kernel, UEFI or whatever that obtains and verifies the actual payload.
You have that OS kernel or UEFI as source code, but you don't know if the source code contains a backdoor unless you either verify it manually, or have it verified and signed in some way by a third party you trust, and there the whole signature thing comes back.
(BTW thanks for the discussion. I'm really enjoying this!)
I was thinking an FPGA with an open toolchain might make a pretty solid hardware seed that can fairly easily be replicated, without needing your own fab or anything completely impractical. In theory the FPGA could still try to recognize and backdoor a bitstream right when you load it, but practically there's a whole bunch of different open-source cores that you could load on the FPGA, and it would be very hard to try to recognize and backdoor all those potential designs at the netlist level, or at least it would take a suspiciously large area, potentially visible as clearly more complicated than what should be needed on a microscope.
You could maybe distribute these verified boards that are just the FPGA and the verified CPU core + kernel + software seeds all stored on a basic NAND flash. But then instead of writing a lisp interpreter in machine code as your seed.. the seed would have to be an entire basic CPU that runs something like hex0, or like a basic lisp machine. You'd plug a keyboard into it and bootstrap the rest from there. But good luck with that, I'm not volunteering to try to make all of that work!
Plus there's still a small chance of a hardware backdoor somehow powerful enough to recognize any possible core you can load on it, or that the tools you use to even load a NAND flash or the NAND flash itself could be backdoored, so really we're just displacing the problem a bit further every time. But if you want to bootstrap everything from nothing, then you basically have to jumpstart all of computing electronics back up from nothing.
Isn't a sectorlisp running on a microcontroller a more straightforward solution? Detecting and modifying a sectorlisp on the fly would require something like a frontier LLM with latency on the order of fractions of a second.
>Rather than compressing particles [...] If you packed enough photons into one spot
I haven't watched the video, but if we're compressing electrons, neutrons, or other fermions, I imagine if we want to keep compressing that down to an arbitrarily small radius, won't we pretty quickly find it favorable to shift those fermions to something else, probably photons, to respect Pauli exclusion?
Really, I don't know enough physics to figure out the reason why it shouldn't always end up in this incorporeal energy-curving-space situation either way, if we're compressing arbitrarily far.
> Finding a tame enough special case was how Hawking discovered his radiation.
It's how it was formulated, but the radiation is far too weak to measure to know it's a real thing on an actual black hole; from this calculator, a 1 solar mass black hole has a Hawking radiation power of 9e-29 W: https://www.vttoth.com/CMS/physics-notes/311-hawking-radiati...
We do see analogous effects in physical analogues of black holes, but we don't know for sure that Hawking radiation actually comes off of actual black holes.
Worse, when they're small enough(!) to be luminous enough to actually observe, they should be hot enough to be spewing out a whole load of exotic nonsense particles (not just photons) that we don't really know how to model correctly with regards to Hawking radiation even if it is part of whatever ends up unifying QM and GR.
Given even the event horizon of a BH doesn't play well with QM, it's probably best to wait for some physicists to work out how to combine QM and GR better.
But then you "fill up all the photon slots" too (not literally because they are not fermions, but they do spontaneously convert back into things like electrons at that density) and you can work around the Pauli exclusion principle by stacking your electrons at higher and higher energy levels.
Pauli exclusion isn't an impenetrable force field - as you say, it's just often more favourable to do something else than to work around it. Consider an iron atom with however many electrons though - all those orbitals except the inner one are electrons working around Pauli.
Good news is that they just added a plan stability feature in pg19. It's actually full planner hints, so you can edit the plan to whatever you want if you have no fear, but the main motivation is exactly index stability.
Reading the LLM's 12 MB lean output is a bit like trying to maintain a codebase that has been fully vibe-coded as a single giant file, by hand. Even if it's possible in principle, no one is going to enjoy that.
reply