eab-

The fact that this firm makes such defective environments is certainly worthy of attention, and most likely a completely irreversible reputational loss; however, I found the framing in this article of 'therefore all the P(doom) stuff is a psyop, specifically in order to defend this company' to be completely unjustified and frankly a little insane?

This reminds me of Once Upon A Time in Shaolin.

> courts have found it to be legal

≠ ethical

they're spending like 9 figures on a single marketing agency - this doesn't surprise me whatsoever

Honestly I expect it's just annoyed devs getting annoyed about the ratelimits on plans and post-hoc justifying. Now that Codex has far more capacity and their slot machine makes better outcomes (note: I am a heavy LLM-assisted coder) they feel like they have to justify their felt animosity towards these companies

is there examples of the sort of things that's been built with these systems? it often feels like complication and abstraction for its own sake

I used to have an emoji password for my Android phone, and had the exact same issue after a reset! It's an odd but pretty terrible failure mode for locking oneself out...

> We have proofs that are gigabytes (I believe even terabytes in some cases) in size, but we know they are correct because they check in Lean.

I'm not aware of any of these. There's some SAT-like results that were not verified in Lean at that sort of scale, but Lean proofs of individual problems are nowhere near that. For example, Mathlib (think a Lean4 math stdlib) is 6GB including compilation artifacts, and iirc <100MB text.

> Haha. How do you reconcile a proof with actual code?

Languages like Lean allow you to write programs and proofs under the same umbrella.

I find it surprising that GPT managed to complete (with indeed a harness that doesn't seem very powerful!) and Claude still cannot.

I'd find this article a bit more compelling if it was used to find current introduced bugs, instead of just using a holdout set

My understanding is that also this tail call based interpretation is also kinder to the branch predictor. I wonder if this explains some of the slow downs - they trigger specific cases that cause lots of branch mispredictions.

What do you mean about CLIP?

There's both "no multi-program system" and "multi-program system", depending on how you look at it. In reality, you're always executing the same machine code, itself has no awareness of programs.

a lot of the researchers are still in london

[Joseph Myers (IMO committee) in the Lean Zulip](https://leanprover.zulipchat.com/#narrow/channel/219941-Mach...):

> I talked to IMO Secretary General Ria van Huffel at the IMO 2025 closing party about the OpenAI announcement. While I can't speak for the Board or the IMO (and didn't get a chance to talk about this with IMO President Gregor Dolinar, and I doubt the Board are readily in a position to meet for the next few days while traveling home), Ria was happy for me to say that it was the general sense of the Jury and Coordinators at IMO 2025 that it's rude and inappropriate for AI developers to make announcements about their IMO performances too close to the IMO (such as before the closing party, in this case; the general coordinator view is that such announcements should wait at least a week after the closing ceremony), when the focus should be on the achievements of the actual human IMO contestants and reports from AIs serve to distract from that.

> I don't think OpenAI was one of the AI companies that agreed to cooperate with the IMO on testing their models and don't think any of the 91 coordinators on the Sunshine Coast were involved in assessing their scripts.

The same Google that makes you log in again on like every other `gcloud` call? By copy pasting your password into the shell prompt?

yep, this post is full of this post-rationalization, for example. it's pretty breathtaking

The notifications aren't great, and the non-e-ink screen is a bit annoying. Also the low amount of physical buttons.

But as someone who bought an OG Pebble and now has a Vivoactive 3, I think the fitness features are too nice to switch back fully to Pebble. Although I'll be very glad to see Pebble back!

> Just insist on Lean (or some other formal verifier) proofs for everything

Lean is too inflexible for this, in my opinion. Maybe I'm not dreaming big enough, but I think there'll have to be one more big idea to make this possible; I think the typeclass inference systems we use these days are a severe bottleneck, for one, and I think it's very, very tedious to state some things in Lean (my go-to example is the finite-dimensionality of modular forms of level 1 - the contour integral is a bitch and has a lot of technicalities)

Why do you expect GPT being tuned on Lean will help it for research-level math?