Yeah, I think it’s going to improve a lot. Though, I actually think the Lean proofs only provide so much benefit.

The LLMs operate in a lot of ways remarkably similarly to how we do. It’s just as important for them to be able to “chunk” ideas into coherent blocks as it is for us. Lean code still allows writing what I would describe as spaghetti-code proofs, and doesn’t require building your theory with the sort of coherent building blocks that lets you build high.

I think the real improvements will come as we learn to use LLMs to write more structured and elegant proofs, and at least for the near term, I think that that favors the human language approach over the Lean-first approach.

I’m definitely not totally confident of this, and wouldn’t be shocked to be wrong though.

note that you probably need to trust the remote household with your data

Probably not actually. Borgbackup (and any sensible encrypted backup system really), does client side encryption. So the data should be encrypted before it’s even sent down the wire. The remote household shouldn’t be able to access the data without the encryption key/password.

I mean, they will have to trust the remote household not to destroy the data, but that’s pretty much an unavoidable limitation.

You’d better give us money and not try to regulate us.

Actually, right now, the western AI companies desperately want regulation.

An unregulated environment is one where they’re forced to compete on price against the Chinese companies and startups running open-weight models. All signs point to them losing that battle.

OpenAI/Anthropic’s wish list right now is a bunch of regulation to prevent the use of foreign models, and to require expensive to implement “safety” requirements that make it hard for startups to compete.

I didn’t say that.

Listen, I’ve got nothing against you hating AI. There’s lots of valid reasons to be concerned, especially with the implications for the future of jobs and work. The way corporations are adopting AI is legitimately concerning.

Just don’t pretend it’s about the environment when it’s not. That isn’t just an unconvincing argument, it hurts the environmental movement generally.

It’s the plastic straws all over again. You understand that the stupid straws debate did the environment no favors right? Fighting AI as an environmental issue is much worse because the AI is coming, and you will lose that fight. If you’re arguing for more controls about water and power use, I’m with you. If you’re arguing for a carbon tax, I will sing your praises. If you’re trying to fight the idea of AI itself, and pretending that it’s about the environment, that’s where I have a problem.

The TPM exists because it’s useful to support use cases where you want your passkeys tied to a device. It isn’t a Microsoft thing either. I run Linux - my computer has a TPM. I can’t use it because Linux support for the TPM is weak still, but it’s there! You probably have one too if your computer was made in the last decade.

By default, even on Windows, your website passkeys aren’t stored in the TPM. No one is forcing you to store your passkeys on the TPM.

And they won’t, because it’s a bloody stupid idea that benefits no one.

Microsoft wants your passkeys synced across devices because that’s how you get lock in. If the passkeys are stuck on the computer you made them on, then you may as well buy a Mac for your next computer because those passkeys are gone either way! If the passkeys are in Microsoft Password Manager though, now migrating to a Mac is harder.

You absolutely shouldn’t be angry!

The existence of powerful open-weight models is the single thing that’s going to prevent us from descending into the full corporate dystopia everyone’s afraid of.

It’s going to hit the stock market hard once everyone figures out what’s going on though.

[forget]
keep-daily = 10
keep-weekly = 4

Daily backups are cheap because of de-duplication. I keep a few weekly backups in case it takes me a bit to notice something went wrong. I don’t usually back up logs.

I could probably drop the weekly backups without much risk, but I’ve got the space.

Sure.

Do you think that’s a reasonable reason to hate gen AI?

There are absolutely issues around the rollout of AI. I haven’t seen anyone disagree with that. That’s just not a good argument for being opposed to the technology. That might be a reasonable reason to hate xAI or Microsoft (and I do!). It’s definitely a reasonable reason to have concerns about how we’re doing this. You should be concerned.

It’s not a reasonable reason to hate the technology itself.

You’re free to hate GenAI all you like as far as I’m concerned. Just be honest about your reasons, and don’t pretend it’s about the environment if you don’t care enough to even look at the numbers.

So… your evidence for slop is that he made a patch, they caught an issue in the review process, and then he had to go on vacation so he asked another maintainer to take over to get the change done correctly in the merge window?

How is that not the process working exactly as intended?

The hilarious part is, yes, I don’t care how fast my launcher is.

But… also, Steam is by far the slowest, least responsive program on my computer.

“Faster than Steam” feels like a joke.

I don’t use a lot of non-open source applications (and not a lot of desktop applications generally). Have they gotten so bad that the slowness of Steam doesn’t feel bad to people anymore?

Have you actually looked into the real environmental impact of AI is compared to, say, eating meat, driving a car, or taking a yearly plane flight? It’s a rounding error. Have you looked into the numbers? Compared the environmental impact of your AI use to the environmental impact of taking a yearly vacation on a plane?

The RAM shortage is real, but very temporary. Check the news today! Chip stocks like Sk Hynix are way down because people are worried about over-production. The fact that a new technology caused a temporary shortage in a resource just isn’t even a coherent argument against the technology. There’s discussion to be had here about whether we should as a civilization reserve some resources for other industries. That’s a discussion we could have. But the idea that AI caused a temporary shortage in RAM, so that makes it bad is… like, really ridiculous? You must see that that doesn’t even make sense as an argument?

These are not arguments that hold up to scrutiny. You should consider whether you accepted these arguments because you looked into the details and they actually make sense, or if you accepted them because they’re telling you what you want to believe.

I really hate that that comment is getting upvoted.

People love to hate on things a lot more than they like to understand how things actually work.

To make your point more explicit, CEOs often don’t have to sit for depositions because they legitimately aren’t the people who know the facts the cases turn on. When the CEOs are the right ones to talk to, courts don’t hesitate to make them show up.

Don’t get me wrong, I hate big corporations plenty. Don’t get me started about Meta or Microsoft. But can we please hate them for actually good reasons instead of making reasons to hate them up?

the models only need to be right some of the time and they still constitute a threat.

Right!?!

And with how cheap and fast they are to run, they don’t have to be right that often as long as a separate run can verify/validate claims. In a lot of ways what the LLMs do should probably be thought of as just a very sophisticated sort of brute force approach. You’re effectively just searching the space of combinations of known vulnerabilities. It doesn’t require particular cleverness, just an encyclopedic knowledge, a reasonable way to prune the search space, and the ability to put in the compute time.

I must be missing something, because you’re getting a bunch of upvotes. I don’t disagree with anything you said, but it feels like a total non-sequitur to what I was saying.

Yes - proper air-gapping is a good idea. But asking the big AI labs to air gap is kind of pointless. Liability already gives them legal incentives to avoid incidents. If that didn’t stop them, a letter signed by a bunch of academics sure won’t. More importantly, open-weight models capable of doing all the things that we’re concerned about are already in the hands of bad actors around the world.

This letter is asking us to lock the front door of the house when the back wall is missing.

The ones in Russia definitely are. They don’t have to be local models - you run them in the cloud like anyone else.

The idea that the frontier labs have LLMs with special capabilities that make them dramatically better than the top open-weight models is largely marketing.

The reality is that most systems are poorly secured, and LLMs make exploiting vulnerabilities fast, cheap, and easy. What would have taken a trained security researcher weeks before can be done by a much less skilled attacker with an LLM in a few hours.

This is stupid. Open-weight models that can largely do what the OpenAI/Anthropic models did are already out in the wild.

Do these people not understand that you can’t put the cat back in the bag?

Memorizing passwords doesn’t scale well.

You’ve likely got dozens of accounts. You’re not going to memorize a password for every account. Re-using passwords is a serious security problem though. Poorly secured sites get their password databases leaked all the time. If you use the same password on lots of sites, it’s basically a sure thing that the hashes are out there on the darkweb already along with your email, and your password is compromised.

Also, typing your email password into an unsecured library computer is a terrible idea. It is ridiculously easy for someone to install a keylogger and gather emails and passwords. In the past, your main protection was that it wasn’t worth anyone’s time to break into the computers, install keyloggers, collect lists of passwords, then figure out how to use them to get money. But with LLMs that can all be automated. It has become ridiculously cheap, and can be done by someone with a bot farm in Russia.

A password manager largely fixes the first problem, but at that point you need a device with your password manager with you to log in anyway. And the password manager doesn’t fix the second problem at all.

I’m just not convinced that mandatory hardware attestation is actually a real problem we need to worry about.

Like, yes, people with high security jobs will have that for sure. And they should.

But large companies that want customers? They want to make it as easy as possible for their customers to connect. They’re not going to force people to have a hardware device which if damaged or lost will lose them a customer. That’s just not what they want.

And… honestly, you should probably buy 3. Losing your main key only to find out that your backup key broke a month ago and you haven’t been testing it is a real risk.