Or, they crash and burn, maybe taking Anthropic with them too

Which doesn't mean an end to the AI race, since China is unlikely to care whether US companies secure financing

Also, if this happens OpenAI will probably bailed out with taxpayer money

I disagree that they would be bailed out. The contagion and impact on the larger economy would be somewhat limited. They would more than likely just be sold to the highest bidder. The US would certainly dictate that the buyer is a US company, but I don’t see a bail out.

Why would they be bailed out? They aren’t a bank.

The authors of Lean also wrote a smt solver (Z3). Other proof languages like F* use Z3 to prove its things

Why isn't there a tactic in Lean to prove things by SMT using Z3? This could be integrated to grind

I don't care about missing features, but I just want a way to export to latex using typst.

It's okay if this is not the day to day tool used to render, but this should be possible. It's just a compiler between two languages, and latex happens to be Turing complete (and can display arbitrary things to a PDF), so it's 100% in the "not impossible" category

With such a tool nobody has to know if you use typst personally. Just like, say, nobody has to know you use jj rather than git

Made me think. Why not convert Github datacenters into Azure datacenters that have Github as their sole customer?

Then it's up to Azure how they will manage this

That sounds like the worst of both worlds? The Azure devision that can't even reliably can't provide decent infrastructure products based on their own data center trying to do the same one a bespoke data center.

You are supposing that with more productivity people will emit less carbon but there's no mechanism for that

More productivity means the employers just demand more from the workers

Yeah, this seems like a textbook case where one could apply Jevons Paradox.

> I beat Chrono Trigger on a 486 with sound and transparencies disabled. There were parts where I had to manually switch off the top layer because transparent stuff (such as clouds) would completely block my view

Also, you could get better performance running on DOS rather than on Windows

The same was true for gameboy emulators too

Wow, I remember specifically buying a sound card and CD-rom drive for my 486 so I could run the GB emulator. It wouldn't boot without a sound card and I really wanted to play the non-translated version of Pokemon Gold. People wouldn't believe me when I told them I had a newer Pokemon game than Red/Blue/Yellow.

So this doesn't happen in the paid plans of ChatGPT? But why?

Paid plans give you access to much larger, more intelligent models which have thinking enabled (inference time compute). In the example here you can see GPT Pro taking 20-80 minutes to respond with the proof.

All this is far more expensive to serve so it’s locked away behind paid plans.

> thinking enabled (inference time compute)

What do you mean by compute?

I would google or use ChatGPT to a learn more about this, free version should be totally sufficient.

I think it's the opposite, you need to demonstrate that this law would work

1%

Does this benefit people that use uBlock Origin?

Maybe uBlock Origin for Firefox could be updated to make use of this

sounds like it just uses ublocks lists.

though it doesn’t seem to work as well as ublock, the ad slots are still there with just the ad missing so there’s a giant ugly blank spot.

I'd imagine that's the reason it's not enabled by default, they're not finished fully implementing it in Firefox yet.

Probably because they don't leverage cosmetic filtering yet: https://docs.rs/adblock/latest/adblock/struct.Engine.html#me...