twotwotwo

We weren't signed up but as a measure of the scale of this we still wound up with a couple of Imagination Library books through book exchanges or buying used online -- i.e. there are enough of these 300M books floating around that if you have a kid there's a good chance you run into them.

I like the sibling comment "We should be more ambitious with the people we build." -- there are so many great things people with some means can be doing!

Folks really want to decide if this is pro or anti and respond to that. It's neither.

In a world with only LLMs doing the day-to-day of proving, you still want more than just proofs dumped out as soon as they pass adversarial review or formalization. The first proof code that passes checks may be a mess that's hard to build on; the path to a result, including failures, is full of interesting stuff; naming, generalizing, linking, and organizing things are tasks that move us from today's raw material to tomorrow's future directions.

Folks get this about code: "it works" isn't the same as "it's good." We knew it before LLMs, out of practical necessity as projects became hard to build on.

An odd thing to me is it would not be that big a concession for the labs to openly talk about the difference between the math artifacts they're releasing and what mathematicians do. It's analogous to the Claude's C Compiler post noting it wouldn't replace a prod C compiler. They could talk about paths from a rough initial product to 'production' math, say they hope future models will continue to improve as math collaborators and expositors, and so on.

For the compiler, the gaps would be trivially obvious to their customers, so it was an obvious call to acknowledg them. With their math output, the difference between a proof dump and the kind of well-written, contextualized mathematical program the community pursues is apparently subtle and deep enough the companies can't get themselves to acknowledge there is any difference. So the companies self congratulate and then are yelled at on the Internet instead.

(Ant seems to have wised up a tiny bit about this compared to OAI, and e.g. Ant handed a recent result to some experts in complexity theory to understand and refine and publish rather than just dumping a Claude-written PDF.)

And yes the drug discovery piece was weird. There are good relevant points: it'd be good to understand pharmaceuticals better (helps us find others, understand side effects, etc.); when we get a mystery result, it's worth effort to try to work our way to proper understanding; anything that could help us understand (reasoning etc.) shouldn't be hidden. But as presented it's both not a lot like math and accidentally a lot like those "would you choose..." questions that always get so much engagement on social media.

Yep, it's unfortunate how often folks sort something into pro or anti then reach into their bag of anti or pro arguments without relatively little attention to the specific thing they're talking about.

I am always uncertain about impressions, but mine agree with this. I liked Luna 5.6 on Amazon Bedrock (which got >100 tps) for doing well-specced tasks fast. 6 seems to both be served slower by Bedrock and may spend more turns/tokens to get to the same place, so...not as fun.

And, of course, GPT-6 came out as Anthropic fixed a bunch of stuff with their models -- faster (via fewer tokens, and TPS for Sonnet), easier to work with, better results, cheaper (via pricing and, again, fewer tokens). I don't know if the timing and the suddenness of the improvement on Anthropic's side sharpened the vibes comparison this round, but Internet opinion went pretty clearly to Anthropic.

FrontierCode's results make it look like Sol-6.1 may slot in well where you'd use Sonnet or Opus's low effort.

One thing I don't think any of this reflects is that many well-specified coding tasks, including the self-testing and doing research and tracing out dependencies and so on, aren't really bleeding-edge now: Luna-5.6 and small open models handle them fine. Stuff like "why is this box dropping connections?" or "here's a thing I want you to model/figure out" can benefit from bigger models. But far from everything does!

Making things understandable is part of intelligence as much as producing the initial artifact is. Even if the proof checks out in Lean (or the code runs and passes QA) if it's a mess, it will be hard to use it to do anything further.

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.

About the argument that a beam's strength:weight ratio worsens as it grows: do the artificial structures humans use, like house frames or bridges' trusses, recover strength:weight ratio? Would a theoretical giant with a skeletal structure like a bridge or a house's frame be better off than one with a human-like skeleton of the same material? (And, related to another comment here, guessing the actual structure of bone produces some improvement relative to something solid?)

Hard to make big predictions, but it sure looks like at least this level of capability is going to be available in the open and relatively cheap to run.

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.

One read is 1) they're getting a lot of traffic for Flash, 2) they've said they're updating Pro soon and expect that to lead to a traffic spike for Pro, but 3) that would leave them overloaded, so 4) they're going to raise prices to avoid it.

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.

I think this rates as too obvious to say among anyone remotely close to this, but worth noting there is a lot of distance between an exploit and any real confusion.

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.