This does not only matter doing cutting-edge mathematics. This, about the 'digested' version versus the original, should feel familiar to some folks here:

> This formalization is more streamlined than the original formalization (it has about 15,000 lines of code, compared with around 90,000 for the original proof).

and if you've ever tried to turn an overly vibed piece of code into something that makes sense:

> it has taken me several days (with heavy AI assistance) to perform such a digestion, to place the proof in proper context with previous literature and to simplify and streamline the argument to highlight the main ideas

If you see something that is confusing or overly clever, please don't assume it must be for some good reason you don't understand and move on--ask questions, get it simplified, try to get it worked out. Future you will appreciate it.

The 'floor' has gone up: today's model a bit behind SOTA is like model releases that were blowing people's minds a few months ago. Compared to, say, DS R1, this is far out stuff.

This, Luna, and (if it's good in practice) Laguna S are also fast and light not just cheap. And, as happened before, DeepSeek's first but other open model makers likely follow.

And a small, fast model taking small steps is...fun? More like working with code.

It's interesting that most open models adding 1M context did it in a way that reduces KV cache size (though DeepSeek was the most aggressive, using compressed attention on all layers), but only a couple providers turned it into a discount on cache reads.

Making things understandable is mathematics, and more generally a kind of intelligence, and is crucial to continued progress. You couldn't use algebraic geometry to disprove a conjecture if people hadn't organized (what could have been just) a pile of random observations into something called algebraic geometry.

Historically LLMs have done best where it's possible to train using an objectively verifiable reward function. Computer programs are pretty good on this front and so are Lean proofs. (Of course, they don't only do things you can RLVR heavily, but those have progressed fastest.) Not sure where 'making mathematical knowledge more understandable' falls on that spectrum.

Understandability isn't only important for advanced math. Keeping computer programs from becoming a mess is a challenge in high-level organization too, and the chat with the user is an explanation task. If you look online at what people say about large LLM-built codebases (SlopCodeBench is a neat effort to make make it concrete, but common wisdom seems to mostly agree on the general problem) and chatbot prose, I don't think everyone considers those solved problems!

It's hard to tell how thoroughly the labs grasp and care about this at an organization-wide level. I'm sure at least some maybe-results exist inside labs but haven't been published because the humans couldn't verify them and didn't want to be embarrassed with a false result. (Maybe also why counterexamples are a lot of the first results published: often simple to verify, even if hard to obtain.) A good sign would be if results in a few months come out more like what mathematicians consider well-written papers explaining results in a more intuitive way, fewer shocking announcements of bare counterexamples in tweets. It's probably a slow climb to get there.

For anyone curious, there's a Tiny Desk Concert of songs from the album at https://www.youtube.com/watch?v=o9PoZ0Vcb_s and an interview, in English, at https://www.youtube.com/watch?v=WcQbB7Dc83U

(Shared this on another post of the story last night, figured I might as well here, too.)

For anyone curious, there's a Tiny Desk Concert of songs from the album at https://www.youtube.com/watch?v=o9PoZ0Vcb_s and an interview, in English, at https://www.youtube.com/watch?v=WcQbB7Dc83U

Proofs aren't generally machine-read-only. An exploit of a proof system kernel doesn't necessarily look like normal proof code. Exploits can be fragile: 'safe' tweaks break them. If an exploit used maliciously is found, the person sneaking it through wouldn't exactly be thanked for it. And the window for exploits overall seems to be shrinking: Lean/nanoda are easier to secure than, say, Chrome.

If someone wanted to deliberately sow confusion (my career advice is not to do that!) they would probably have better luck with a subtly wrong formalization or an informal proof. If they have prover kernel bugs, they should report them and get free T-shirts.

Still, it's cool to see how they're hardening Lean.

https://leanprover.zulipchat.com/#narrow/channel/270676-lean...

A mathematically-inclined reviewer (or an LLM) can quickly identify that it's an exploit. (Two exploits; it's crafted to hit a bug in another proof checker, too.)

The post gestures at this, but a natural follow-up, beyond fixing specific bugs around this exploit, would be to task some security-oriented models with proving False in Lean, or with reviewing the code for potentially unsound steps, missing checks, or even useful 'hardening'. That's happening and bugfixes are landing as a result.

DeepSWE will let you chart turns taken or tokens used, and FrontierCode will chart tokens. If you use that, you can see Sol high and Terra max get about the same DeepSWE number, but Terra max takes twice the turns. Luna max scores a smidgen lower with even more turns.

Smaller models relying on lots reasoning may "scale down" better on easier tasks, because unlike size, reasoning effort is dynamic: the model can see the task looks easy and stop. On DeepSWE, the cost curves for the three 5.6 models are almost on top of each other, but on FrontierCode Extended, the version of FrontierCode with the most everyday tasks in the mix, there's a spread of costs at the ~55% level.

The recent Laguna S 2.1 model (118B, 8B active) puts up surprising coding numbers for its size, and the lab behind it specifically credits its "way of working (persistence, verification, willingness to backtrack)". Some other open models that folks report getting good mileage out of seem to get there partly by throwing a lot of reasoning at the problem.

There is a little bit of a question, if some models rely on getting it wrong a bit more at first and external checks catching the problems, of whether they're also more frequently getting things wrong they can't self-verify (say, quality of UI or API design) and then it falls to the human to find it. Still, getting the results they're getting at all is neat.

Some benchmarks historically favored reporting only on the max variants, maybe because they want to show the frontier? but that is not always what you need for practical decision. (AA has the full effort sweep for Opus 5 and Sol/Luna/Terra at least.) And at least FrontierCode finds Opus 5 taking a hit in performance above 'medium'.

I am not trying to pick a winner here. I'm probably not going to use tiny models on max for everything, but I think it's cool that you can get so much more out of a small model by amping up reasoning, tool use, and persistence.

One sort of wild idea: 'give words a color'. That is, the harness/API adds a signal to the input vector (using a few 'role' dimensions or just adding some other vector to the embedding vector) to tell the model the role of an individual input token. It'd be kind of like how positional info is added. It might make some things a little weird--its output will be 'snapped' to the "tool call" or "assistant output" color when it's read back in, for example, regardless of what 'color' came out of the network. A lot of weird stuff happens in models already, though, and this may be less weird than trying to make them behave as formal grammar parsers reliably with security at stake.

A while back I'd dreamed about this as a way to keep models from confusing different kinds of training data: not all input can be high-quality sources, but knowing that a phrase was seen in a scientific paper/encyclopedia, an opinion piece, a work of fiction, a conversation, etc. reduces the chance of confusion. I know they can pick that kind of thing up from other signals like writing style or context, but exactly those signals that lead them astray in prompt injection, and sometimes even leads humans astray when something's written like a credible source but isn't!

- We wrote a cronjob to periodically DELETE for a retention policy on a table we'd just created. Most senior person on the team reviewed it, looked fine.

- Unusually for us, we prioritize QA'ing a different feature for release, delaying the release of this cronjob and a bunch of other code.

- During that delay, the new table accumulated many times more rows to be deleted than we'd expected during review.

- Release happens. All looks well since the initial delete wasn't a migration and cronjob hasn't run yet; engineer doing the release signs off.

- Cronjob runs, deleting hundreds of millions of rows quickly.

- Next day, replica lag's high and MySQL's transaction history is very high. MySQL keeps transaction history around until purge threads have visited all the affected pages on disk.

- The bad cluster conditions last for days and lead to other problems.

This omits detail and the 'noise' of everything else we were watching. But it gets across how the code and MySQL behaved.

Like most exciting events, it led to multiple changes to avoid a repeat. For retention policies, our new approach was one at the end of PlanetScale's post, to partition and drop old partitions. Transitioning to this from a huge unpartitioned table can be fun!

If a table is append-only and already huge, with lots of rows already past the retention threshold, you might only copy the rows to be kept to the new partitioned table: copy what you can, lock tables, do a last catch-up copy and swap tables. (Roughly the blog's 'performant one-off delete'.)

If the table's merely kind of big, gh-ost or such could allow you to ALTER without causing lag, locking, etc.

At a scale below that, you could run a slow incremental 'nibble' delete while watching server stats, and a step below that, plain ALTERs or DELETEs are fine.

Using partitioning has fun bits, too. In MySQL, the partition key has to be part of any unique index, understandably. But you have to keep that in mind when you're using INSERT..ON DUPLICATE KEY UPDATE and relying on uniqueness to trigger the update. Things stay interesting!

I hear Vitess shops like PlanetScale usually don't run multi-terabyte myqsld instances in the first place: even when physical nodes are big, they run many smaller mysqlds on them. That wouldn't make all this fully irrelevant--huge deletes would still sometimes be worse than copy-swap-drop--but it does seem real handy for taming issues that tend to worsen with mysqld size, like replication lag. All to say, little bit jelly of their setup over there!

Async agents interact on a longer timescale, but they interact. Again, experienced SWEs, consulting agencies, etc. ask questions before and after implementation, accept notes, etc.; they vary at how good they are at it; and how well they do it is a big factor in the success and failure of projects.

LLM interaction ability isn't saturated or mature; asking for point edits mostly works, but e.g. when I try to get Opus to ask clarifying questions or surface tricky bits to focus review, it's not close to a human-level response -- it's both noisy and misses key stuff. (Handling uncertainty has been a weak point for LLMs since early on, which might not help.) Other aspects of good interaction are even harder, like digging into a potentially mistaken request, or proposing a good 80/20 tweak to the spec.

There's a different, shorter-term reason to model interaction: it better tells users the value to expect now. It turns out my employer doesn't love infinite Opus use. (Go figure.) Kimi and Sonnet do comparably on FrontierCode. Are they about the same to use, or is one flailing while the other one just needs a couple rounds of fixups? If I saw a benchmark that credibly approximated 'this model will save you this much time vs. that one' that would put it well above existing ones.

I do think a bunch of discussion, investment, etc. is based on the idea the industry will essentially be replaced with successful one-shotting with little interaction. The mistake there is to assume back-and-forth is inessential and only happens because the agents aren't that good at coding yet. For a long time lots back-and-forths were driven by the models' limitations at raw coding, which might've made that idea more appealing.

As the coding side gets better, drawing the rest of the owl becomes the hard part. The world is messy and so is one's software's boundary with it. (I'm not saying the tasks don't get longer, I'm saying interaction gets more important as they do.) My conviction here might partly because in my sort of work the requirements and big picture were always thornier than typing the code; I'm suspicious that as raw coding gets easier for everybody they will hit something analogous.

Anyway, again, what y'all are doing is progress. I do want to stick up for the idea that a lot of critical things aren't raw coding ability. (I'm not alone in that, I don't think!) I'm definitely not here to say someone's Doing It Wrong as they do it more correctly than I've seen it done--just asking "would the patch get accepted?" is a huge step.

Not saying FrontierCode should've done this, but benchmarking the interaction would be interesting. That is, if I get a diff with a blocking problem but writing a comment gets fixed, that's a lot different from if the model has hit a wall. Better, if there's a problem but the model flagged it in a short list of questions or worries to me before or after coding, it can get sorted without taking much of my time. Stick an LLM in the loop instructed to behave like a user or reviewer with some rubric-ish info that wasn't in the prompt. Then, look at how much the pretend user has to do to get to a quality result with a given model, if they can get to one at all.

You could say 'why worry about interaction? the goal is the model just gets it perfect' but I think that imagined end state just is not a thing: tasks will get bigger but there will still be interaction. Handling comments and asking good clarifying questions when needed are real capabilities. Human SWEs interact plenty and real engineering has a certain density of questions about requirements, taste, and other big vague things.

DeepSeek and Xiaomi's deals on cache reads go with their models' latest gens making caching cheaper (using less space for KVs). No open-model inference provider has decided to match the pricing. I'm sure that says something about how inference pricing works, but not completely sure what.

Agree with others that top open models aren't on the frontier, and I would expect differences doing big-picture planning or anywhere you're only giving broad brushstrokes and looking for a lot to be guessed. But they do seem fine at coding from a a concrete plan! No experience in huge codebases because I only use them outside work, but they seem good enough about gathering info before they dive in that I'd expect them to grep around as they need.

An annoying caveat: individual subscription plans, used heavily, are much cheaper than the API -- see https://she-llac.com/claude-limits -- which complicates any argument about cost. I still think open models are worth playing with. They're one of the things that let us treat this as a technology rather than just as the product offerings of one of a few companies.

Humans can do an impressive amount of generalization from one error or surprise, and as is often rightly noted, don't need trillions of words to get going. And it all seems to happen some 'forward-only' way, without backpropagation -- we don't have AdamW or MuonClip helpfully nudging our synaptic connections towards whatever would have scored well on our most recent test. It is relevant that we're creatures with goals -- reinforcement learning is the only stage where there's a taste of that for neural nets -- but the learning differences seem at least partly independent of that.

I suppose it could turn out that, even if not sufficient, the large number of synapses is necessary to all this, like we're effectively buying a lot of lottery tickets that give us a shot at fishing interesting hypotheses out of the experiences flowing by. But I'm still awfully suspicious that we don't have the right mathematical model for learning messy ideas all worked out yet.

That doesn't mean anything's practically wrong with the fielded ZK proof systems, just that's how you reconcile the article's "no non-interactive proofs under these assumptions" with people out in the real world using non-interactive proofs.

This paper brings up another logical possibility, that there could be a non-interactive proof with no RNG or setup that doesn't meet the precise original definition of zero-knowledge proofs but is zero-knowledge practically speaking. I don't know whether we'll actually see better fielded ZK proof systems come out of this approach!

On the other hand, current part prices are not neat; a commodity platform only helps so much if none of what you want put in it is affordable! And other factors like power and cooling can push you away from optimizing for density. I just like that along with the ludicrious becoming possible, merely great stuff becomes more feasible.