It will probably be a future. My guess is that for many businesses it will still make sense to have more powerful models and to run them centralized in a datacenter. Also, by batching queries you can get efficiencies at scale that might be hard to replicate locally. I can also see a hybrid approach where local models get good at handing off to cloud models for complex queries.

> For many businesses it will still make sense to have more powerful models and to run them centralized in a datacenter.

Agree, and I think of it this way: for a lot of businesses, it already makes sense to have a bunch of more powerful computers and run them centralized in a datacenter. Nevertheless, most people at most companies do most of their work on their Macbook Air or Dell whatever. I think LLMs will follow a similar pattern: local for 90% of use cases, powerful models (either on-site in a datacenter or via a service) for everything else.

I like most ligatures, I wish I could selectively turn off just this one.

As AI gets better the bottlenecks will be the place to watch. Bottleneck jobs will become more productive => they either pay more or more bottleneck jobs will be created or some in between situation occurs. This will continue until no bottlenecks are left.

Just want to +1 this. It is a game so good I bought (and beat) it twice, once on Switch and once on Steam.

I just wasted 15 min playing this morning. Can't wait for mosh support

> Does snakes.run support alternative clients? > Not currently. We're interested in supporting Multiplayer Online Snake Home (mosh) in the future.

You can think of theorem provers as really crazy type checkers. It's not just a handful of tests that have to run, but more like a program that has to compile.

Yes exactly. There is this thing called the “Curry-Howard Isomorphism” which (as I understand it) says that propositions in formal logic are isomorphic to types. So the “calculus of constructions” is a typed lambda calculus based on this that makes it possible for you to state some proposition as a type and if you can instantiate that type then what you have done is isomorphic to proving the proposition. Most proof assistants (and certainly Lean) are based on this.

So although lean4 is a programming language that people can use to write “normal” programs, when you use it as a proof assistant this is what you are doing - stating propositions and then using a combination of a (very extensive) library of previous results, your own ingenuity using the builtins of the language and (in my experience anyway) a bunch of brute force to instantiate the type thus proving the proposition.

Technically, it isn't an isomorphism (the word is abused very often), and there is no fixed, general syntactic correspondence. However, in the case of Lean, we can establish a correspondence between its dependent type system and intuitionistic higher-order predicate logic.

For what its worth I use the Microsoft SwiftKey on iOS and I am a fan!

Surprised that with ~6k words I am already in the top ~5%. I guess the old 90-9-1 rule roughly holds up.

I feel uneasy about werewolf being included here. I don't want AI labs to actively try and make their LLMs deceptive!

The one advantage of monopolies is that they tend the commons.

You're free to start your own space exploration company.

Er, no, you're not. That's the big problem with monopolies that execute regulatory capture.

Sure you are. SpaceX did exactly this and went against the well-connected monopoly at the time (ULA, a consortium of defense contractors) and beat it.

Nobody said it would be easy though.

You too can start your own space exploration company if you are lucky enough to somehow obtain capital and your luck compounds sufficiently from that capital.

That luck is out of grasp of the vast majority of the population. It isn't a matter of effort, but mostly luck. Playing the lottery is not a realistic strategy to put forth from a monopoly competition perspective. 90% of startups fail, for example. They worked hard, but were unlucky.