I believe though it is an old phenomenom that if (given the default context) you ask a random number, it will more often than not give numbers from a very small set.

I just used a "Temporary chat" with ChatGPT twice to "Give a random number" and it gave 42 both times (this shuold be rather understandable why it ended up with this). Then I asked "Give a random number in 1-10" twice and it responded with 7 for both (and this too is an old "magic number").

Dropbox switched to it a decade ago, so it's probably quite product-ready.

However, why not switch to the Rust lib when it was available? I suppose people at Dropbox are now pretty happy they did in 2016: https://dropbox.tech/infrastructure/lossless-compression-wit...

It's slower, though. Too high a price to pay for safety it seems.

- either that the claims are paired as you say (the second one implying that the program cannot be fixed),

- or that the claims are completely distinct, that simply state the desirable state of things.

Using the second interpretation, the corollaries would be:

- there is (typically) no reasonable fix for the C++ compiler that would address the UB. Therefore to fix the UB all C++ programs exhibiting the same need to be fixed, which is hard, as the compiler will keep accepting them.

- once the Rust compiler is fixed, then all safe Rust programs exploiting the bug must now be fixed, or the compiler will reject them.

What I would sign under would be the second interpretation, not the first one. But I intentionally also selected the particular ambiguous form due to the cutesy, albeit misleading, symmetry of the statements.

Astra Max can do 12%: https://balrogai.com/

Though after improving the harness it can fare better, but still no completion: https://roger-creus.github.io/blog/astra-craftax-nethack/

I hold the argument that if the Rust compiler produces unsound behavior for safe Rust, then the compiler needs to be fixed.

The point of course was not that what you can do, but what you should do. All cases of safe Rust compiler producing unsound code should be fixed, but the same argument is more difficult to make for C++.

Sometimes should might be different of what you must. For example, if your program exhibits unsound behavior in safe Rust (or C++) code, it's probably a lot more practical to just change the program so that it doesn't, instead of updating the compiler, unless you happen to be a Rust compiler developer. But, at the same time, you should file an issue about it.

You can of course find C++ compiler bugs as well, although I expect that to be quite rare nowadays. But the typical case is that if a C++ program exhibits unsound behavior, there is no reasonable compiler fix for it.

Then there's of course Fil-C! This improves the situation greatly by converting most interesting cases of unsound behavior into runtime errors. It seems not everyone is happy with the runtime costs of making this happen, though. And you must compile everything with Fil-C. It doesn't work with Windows or MacOS either.

- If a compiled C++ program has unsound behavior, the program needs to be fixed

- If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

E.g. OpenCode can be used with all three methods. Looks like it needs a plugin for the two Claude methods, though.

It does say "develop (or to facilitate the development of) a similar or competing product or service", but I think it would be a long stretch to say that's the case if they would just publish benchmarks. Microsoft legal department might disagree.

> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.

So it suggests that the formalization/verification step may have fixed some issues in the natural language proof, and either such differences were never noticed or the corrections weren't ported back to the NLP.

I suppose it was too convenient.

I find it extremely unlikely LLMs would have the monopoly on this particular word arrangement—and indeed they would have learned it from training material produced by people in the first place.

Of course, it still allows the risk that you don't actually get to understand it.