They could probably vibe-optimize it if they cared.

What would happen if they give an equivalent agent swarm the proof and a target to reduce runtime .

Let’s start with “what would happen” and run the experiment instead of starting with “they could probably”.

What would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...

I was replying to the comment about it being slow to run. I wasn't commenting on understanding it.

Then run the annealer and learn from the result.

If they aren't already, or if its possible, prove that an optimized version matches the simple version...

I've recently had great success running codex in a regular qemu VM and using codex remote control to talk to it from my phone.

Honestly works extremely well as a personal assistant.

I can see why turning it into an API makes sense, just be aware you might not need to lock yourself in if you can setup your own VMs.

Yes, I do the same with Claude Code. Create an instance on the server for a project and then can create sessions from any device, close my laptop while claude code keeps working, etc. without losing the convenience of dedicated apps.

The key here is that they are _not_ just turning "running codex on a VM" into an API. Their harness is running outside a VM, interacting with a VM when needed. See the diagram in their post. This allows them to scale the agent runs independently from the VMs. That's why they call it "managed Codex harness", it's a different version than what you run.

I do the opposite. I have a Slack bot that communicates with an app on my Mac mini that dispatches agents for tasks. It knows all my projects and also has a scheduler that uses the Herdr API. That way I can have things running on my Claude/Codex subs at home 24/7.

Setting up all my code, environment, context, etc in the cloud on VMs seemed like a lot so instead I send back tasks to my Mac mini(s) that are running at home.

Yep I run `claude remote-control` as daemons (systemd/launchctl) on whatever paths/repos I wanna be able to create a session from on-to-go.

Works really well and is a great use case for work laptops. Same shell, same memories, same sessions

I've been running Hermes inside a remote docker container connected to Slack bound to a Codex account. It's actually pretty great, I prefer this approach for a lot of things. Because it's in a Docker container I have 100% control over the configuration. It may do some crazy stuff, but I know it's not going to start exfiltrating my AWS SSO tokens or SSH keys from my laptop.

I've done something similar by running pi within an xmpp wrapper on my server, so I can talk to it from any phone or computer. Works super well.

May as well go for Hermes at that stage

Do you have 1 long running session?

Considering the harness needs to be running how else would this work?

Pretty easy these days with old school tools like tmux but more modern tooling like herdr [0] is really the path you'd want to take.

[0] https://herdr.dev/

codex itself has a remote control mode that runs continuously. I wrote a systemd service to start it boot and interact with it via my phone.

But Codex doesn't survive a reboot by default or a laptop going to sleep. Also, herdr is abstracted up a level from the agent, so you actually get more benefit by using Codex with herdr because herdr knows how to operate Codex, and other harnesses. So if you're using multiple Codex instances you can orchestrate them because each harness can talk to the others. You can still interact with Codex running in herdr via remote control (ideally you'd target your "orchestration" Codex instance). It just gives you way more power.

> Considering the harness needs to be running how else would this work?

you can just make new sessions for each new task?

i tend to do this, or at least every so often.

i just give it a config (agents.md etc) to where it knows what's going on, or can figure it out

Codex remote control serve can run continuously.

Sometimes start a new chat in the phone app, sometimes just add to the main one. Both seem to work ok.

If I want the agent to wait for something I need to start a new chat in the iphone app.

if I look at the timestamps, it appears Sholto is the one mocking Noams tweet... Noam posted first.

Douglas' 6:59 AM UTC post is edited. He has a 6:22 AM UTC post that predates Brown's 6:47 AM UTC post: https://xcancel.com/_sholtodouglas/status/209720900556759874...

Also note the lower post ID in the URL.

Doesn’t matter. People’s minds are already made up, and facts aren’t getting in the way.

Assuming that your mind is not already made up, and that facts aren't getting in the way, do see https://news.ycombinator.com/item?id=49608972

I think the new Astra computer use demos show that the models might be able to do things like inspection of real world objects if given a camera.

Super excited to see real world feedback added into the agent loops we have gotten used to working with. Could you let the model print and test the circuit boards it is prototyping with a jig?

In July I was struggling with writing DIY Rust firmware for an e-ink screen. I mistakenly thought I'd ordered an Inkplate 6 ED060SC7 and actually had the later version, which confounded my efforts. I was also mistaken about the pixel resolution.

The way I found this out is I propped it up next to a webcam so it was more or less full frame, and I had the (then new) Fable write a python script to bezier warp the camera capture to a flat projection of the screen. At that point I couldn't address the whole screen. Once I'd guided the capture script I just left the LLM overnight with the instruction to get full control confirmed by a capture round trip, and it was meaningfully finished in a couple of hours. I don't really have the skills to attempt that myself in a reasonable time frame.

I don't know about pcbs but i gave chat gpt a picture of my window to help design a mesh screen frame to hold the feline hostage in, and it gave a fairly convincing impression of understanding what was going on, although at one point it thought the window swung inwards (it's an outie).

if that is true then why is astra on the official ARC leaderboard now ?

ARC leaderboard has results from semi-private data for frontier models, they have another competition for private data.

It is described in their methodology: https://arcprize.org/policy

It makes sense, since once OpenAI API receive task, it is not private anymore but leaked to OpenAI.

Where are results for private data?

Which LLMs participate on private set? Open weight LLMs only?

Yes, they run competitions once a year amongst open weight models

I think the security aspects are overblown... but being able to edit the code of any part of your system is very useful.

Would love to see someone try to automate the bootstrap chain from a working C89 compiler to Rust.

At this point I think current LLMs are able help these incredible feats of bootstrapping as they can grind out the impossibly long built times over multiple days/weeks.

I am very optimistic for deterministic builds in general.

I am working on this![0] But this is actually a herculean task, I've been chipping at it for weeks and even trying to cheat somewhat by translating mrustc from C++ to C89. If anyone has ideas/cheaper ways to run it I would like to know.

In the meantime, months ago I achieved bootstrap of TCC (then GCC 4.6) via the same path as the live-bootstrap project but replacing the Scheme part with a C compiler in Ben Lynn's Haskell dialect.[1] This was a project I wish I had time to do years ago[2] but never had the time or motivation for, and the type of things agents can do well now (they couldn't write good Haskell a year ago).

[0] https://github.com/siraben/mrustc/tree/siraben/cmrustc

[1] https://github.com/siraben/blynn-bootstrap

[2] https://logs.guix.gnu.org/bootstrappable/2021-05-26.log#1438...

> If anyone has ideas/cheaper ways to run it I would like to know

GCC 4.7.4 was the last version of GCC fully written in C, with full C++98/03 support and a decent subset of C++11. As far as I know it is used by the bootstrap project presented in the article.

Specifically the expensive part is getting a C89 port of mrustc to compile rustc 1.90.0. mrustc needs C++ right now, bootstrapping via TCC by writing it in C89 would be the shorter chain.

Sounds pretty difficult (if not impossible, see cfront 4.0) to translate C++ code to C89. You have to keep track of all constructors and destructors and their progress along the body yourself, and I assume it must be fit for exceptions as well?

Yes, this isn't meant to be a complete port and I only started dipping into mrustc because the previous agents were going off the rails. I have mostly been throwing spare weekly quotas at this but deeper thought will be required to get an actual working Rust compiler in C. Rust is an enormously more complex language, so it might just be at the capability limit.

> Rust is an enormously more complex language

I have no doubt that a Rust compiler can be implemented in C. But it's a different project to write one in C from start than trying to migrate an existing C++14 based project to C. The former is likely "easier". An alternative approach could be to migrate the C++14 code back to C++98 and get rid of the exceptions, which makes it transpilable to C (using the cfront approach). Though the result might not be maintainable C, but still C.

EDIT: if you manage to migrate it back to a sufficiently moderate C++11 subset, or even C++98, you could use GCC 4.7.4 to compile it, which itself is written in C.

Thanks, will look into this as another avenue!

> Would love to see someone try to automate the bootstrap chain from a working C89 compiler to Rust.

We did that in stagex over a year ago actually and several major orgs are using it in production. Also no dependency on libgcc. LLVM native. We presented it at Open Source Summit and Linux Security Summit this year.

Clone https://codeberg.org/stagex/stagex and run "make core-rust".

Will build "FROM scratch" in containers from hex0 to recent rustc.

Closed models don't even need a back door - they will just MITM you and replace your code with malware.

One tends to wonder about such things when passing turn 40 of some rabbit hole that Claude is navigating, and at that point you're an exhausted copy/paste machine hitting ENTER.

Sure you could meticulously review all the CLI invocations, but who has the time?

Right, but I think everyone knows this. It's less obvious that a "fully locally run" model could pull a stunt like this.

(Your OS, or your device firmware, or even your CPU could be doing the same thing.)

I doubt anyone announces when they have under billed. OpenAI has also done many low price deals and quota resets.

But you have eyes, right? And a brain, and live through your own experience and can reason about it, right?

When was the last time someone undercharged you or didn't charge you at all by mistake?

Is this a common occurrence?

What's the proportion of overcharges vs. undercharges you have observed in your life?

Usually it's user's incentive to control over-billing and company's one to make sure there's no under-billing :)