About a year ago, David and I put up two bounty problems involving natural latents. I am now about 80% confident that both have been resolved, both within the past couple months. Both cases made heavy use of LLMs and Lean.

The first to land was Grisha Pochuev's counterexample to the "Existence of a Deterministic Maximal Redund" conjecture. It's pretty readable, and I'm mostly convinced that it works. The original bounty post offered $500 for a proof or partial payout for a counterexample, with partial payout depending on how thoroughly the counterexample killed hope of any nearby variant of the conjecture. I think this counterexample is worth $300. Good job Grisha, and hopefully I can figure out a not-too-painful way to send you money.

Meanwhile, for a couple months David has been cranking away on "secret project X", with the promise that he'd tell me what the project was if and when it bore fruit. Well, apparently it bore fruit; he now has a proof that existence of a stochastic natural latent implies existence of a deterministic natural latent, which was our other bounty problem. The proof is apparently "pretty gnarly", lots of cases, all LLM-coded in Lean. I have not looked at the proof at all, but I'm operating on the assumption that it works and I'm hoping it will be simplified a lot in the coming weeks.

... and while all that was going on, I've spent the last few months mostly doing interp experiments. Some time early this year, Claude Code reached the point where it can handle my day-to-day interp coding needs well enough that I never need to write the code myself, which has been a qualitative jump in usefulness. Claude's interpretations of results and suggestions for next steps are still mostly useless, but it can at least write the code, and (I think) I can usually tell by looking at graphs/tables of outputs if the code is wrong.

So across the board, LLMs have started to meaningfully accelerate our work within the past ~4 months.

This is all in stark contrast to two years ago, when I reported that:

Basically every time a new model is released by a major lab, I hear from at least one person (not always the same person) that it's a big step forward in programming capability/usefulness. And then David gives it a try, and it works qualitatively the same as everything else: great as a substitute for stack overflow, can do some transpilation if you don't mind generating kinda crap code and needing to do a bunch of bug fixes, and somewhere between useless and actively harmful on anything even remotely complicated.

and:

Over and over again in the past year or so, people have said that some new model is a total game changer for math/coding, and then David will hand it one of the actual math or coding problems we're working on and it will spit out complete trash. And not like "we underspecified the problem" trash, or "subtle corner case" trash. I mean like "midway through the proof it redefined this variable as a totally different thing and then carried on as though both definitions applied".

At the time, multiple people hypothesized that we were just bad at using LLMs. Ray was one of those people; one day when we were coding something and the LLM was failing to help much, we invited Ray to take a look and hopefully tell us how to better use the LLMs. Ray concluded that our coding problems really were quite a bit more complicated than his day-to-day, and LLMs probably were not as good at them.

But that's in the past now. LLMs still do not look close to being able to do all the core pieces of my work, but they are at least accelerating meaningful parts in a big way, enough to qualitatively shift what we do and how we do it.