HotHotLava

Would that change anything about the conclusion? Having a "bug" that changes available model options for some small set of Pro users 3 months after launch certainly qualifies as a wtf-are-they-even-doing level of bug in my book.

"Risk" has nothing to with designing functional and elegant UIs, so I'm not sure why you would even make the comparison.

It means risk that the software stops working after an update. Which usually trades off iteration speed and best practices (i'm pretty sure the average startup has way better security practices by just delegating to google/aws than the average manufacturing software business) in exchange for a rigorous testing and rollout schedule.

So I'm also not sure that the article has a point at all, the human writing the code was never relevant to avoiding the "risk" in these industries in the first place.

"extremely severe" - aren't we laying it on a bit thick here? The whole impact seems to be that users who have telemetry turned off got this feature ~2 days later, when the bug was noticed.

Per the rules link that you yourself post, no, publication must not necessarily happen in a peer-reviewed journal.

Take a look at https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossible that they're hitting some bug, but way harder than one would intuitively think. For starters, they'd have to hit two bugs in two independently written Lean kernels.

In what world is peer review a higher standard than formal verification in Lean?

Not in the world mathematicians have been living in for the past decades at least. Nearly all big theorems that have been formalized so far had been published beforehand, and it was usually regarded as a step up in rigor. Wrong results get published in peer reviewed journals all the time.

I feel like there's a pretty huge difference between using inputs and outputs as part of a general training corpus, and looking at a specific users workspace after hearing rumours and yoinking their ideas to beat them to the point.

Unless OpenAI finished a whole new training run on the latest data in the last few days, the possible allegation seems to be the latter.

The nice thing is, once all of these proofs are formalized in a machine-checkable language, it should be relatively straightforward to translate the corpus between different languages, if someone finds something with a nicer syntax.

What would be "noise" in this context? Random words, random sentences, random complete short stories?

How do you "easy" VPN into the US in 1995? The whole consumer VPN industry didn't exist back then.

I think you're vastly overestimating the average persons ability to use Blender if you can do that in an afternoon; just figuring out how to place a colored cube and the camera probably takes an afternoon if you pick up Blender for the first time.

Given that the pelican looks way better than the dragon, it almost seems like a certainty.

Usually I wouldn't expect anything to happen to a big company like this, but oof...this is so much worse than the title makes it sound. If they leave something like this in their store, then all user trust will be gone.

I'll bet there's also a good number of developers at Anthropic itself who are now surprised to learn that every api token etc. that may have appeared in a Claude Code bash command is now leaked to a third party. Whoever can gain access to this telemetry server is sure to find a lot of valuable stuff in there.

Well, yes, it is. That's why you're seeing them take proactive steps to address the problem, like this new policy.

It's an ironic situation; logically what should be the moat are the models, costing hundreds of millions of investment cost to train and operate so it would make sense if we see different provider focusing in different directions.

But right now we have 3-5 top contenders that are so evenly matched that the de-facto sticking point is mostly the harness, ie. the collection of proven plugins/commands/tools/agent features that are tuned to the users personal workflow.

Do you not know how ebay works? You put in the maximum price you're willing to pay, and if you win you're paying 2nd highest bid + 1. So you don't save any money by starting with a low bid.

Basically every AI agent released in the last 6 months can do this pretty well out of the box? What feature exactly are you missing from these?

It'd be equally hilarious if that VC money would be used to actually better society by crushing GEMA in court.

But realistically, all that will happen is that the "Pauschalabgabe" is extended to AI subscriptions, making stuff more expensive for everyone.

Please don't pretend to be dumb, "predictable" in this context means that you know the final price of the trip before you start the journey, instead of having an odometer.

And randomly hoping for a taxi to drive by maybe works as long as you exclusively travel between airports, train stations, and downtowns of major cities, but if you're even slightly more remote than that you'll have to call or use some random app to get the Taxi to pick you up.

Taxis and B&Bs and Hotels all still exist and compete with Uber and AirBnB.

Even at the same price there are valid reasons why many people prefer an Uber over a Taxi, in particular the predictable pricing and globally consistent UI.

If the problem starts to become big enough, I'd expect airsoft venues to offer special streaming or non-streaming times, depending on which group is bigger. Similar to how Saunas offer special clothed or women-only days.

H200 rental prices currently start at $2.35 per hour, or $1700 per month. Even if you just rent for 4h a day, the $200 subscription is still quite a bit cheaper. And I'm not even sure that the highest-quality open models run on a single H200.

I'm pretty sure OP wasn't talking about the management hierarchy, but "from the top" in the sense that it was big established companies inventing the cloud and innovating and pushing in the space, not small startups.

For me, I actually feel much more motivated to write good and accurate documentation knowing there will be at least one reader who is going to look at it very closely and will attempt to synthesize useful information from it.

Same with my old open-source projects, it's kinda cool knowing that all the old stuff that nobody would have ever looked at anymore is now part of a humanity-wide corpus of useful knowledge on how to do X with language Y.

That's why it's just "mostly" false, but 'empty' is a word with a specific meaning, and claim here was that the port is literally empty of ships. (or, in the case of the Twitter message they show, that there's only one single ship in the harbor)

Sure, but then it's less of a fun side business and just becomes straight up smuggling.

The playbook is obvious - if Trump loses, Vance refuses to certify the election results due to "fraud", Republican states will produce alternate lists of electors that vote for Trump, and he will claim that in reality he just won reelection with the biggest margin in history.

How do we know this isn't just crazy conspiracy theory? Because they already did attempt the same thing in 2020, and this time they had the chance to vet the VP candidate for this scenario.

That comparison also shows that a recognizable brand alone can easily be worth more than 100 billion; Coca-Cola also has competition that offers similar products and zero tech advantage, but they still managed to keep their number one spot for decades.

Used to. If they're going to start a trade war, pull out of NATO and invade Greenland instead, there'll not be much soft power left to drag Europe anywhere.

The literal first sentence of the announcement is:

> The Stargate Project is a new company which intends to invest $500 billion over the next four years