Viewing profile — nilkn

In some cases you're right, but I think that's often a symptom of mathematics in Lean being relatively immature (i.e., it will get much easier with time). Even then, verifying the …

I'm just barely old enough to have experienced a couple waves of technology being introduced and creating these sorts of life optimizations. It almost never actually improves quali…

This is the Lean proof that a nonsofic group exists (34,440 lines): https://github.com/openai/ten-proofs/blob/main/NonSoficGroup... This is an extraction from that of the actual th…

I find people's view is based on how much they're personally "winning" financially. If they're making money, then daily life seems more about building. If they're not making money,…

Couldn't care less. I'm not reliant on anything you just imagined I'm reliant on that supposedly doesn't exist, yet somehow I'm reliant on it. I use the Vision Pro for Mac Virtual …

The overwhelming majority of people don't want any VR device available today at all. I'm perfectly fine being the minority for now. You say that as if you think I'd have a problem …

For me, the economics are the exact opposite. I'd pay $1000 for a good gaming VR headset, but not $4000 -- because gaming is just a hobby that isn't really worth that much to me. G…

Yes, this is a challenge, but I don't think it's as damning as it sounds. First, the same kind of issue exists with any kind of testing. We all know that having unit tests and inte…

You are free to bow out. However, we are decidedly not nitpicking over minutiae. I don't think you have understood this thread, and that's leading you to make very confident assert…

You gave an example of Linux having value, which is not contested and not relevant. You did not give any examples showing the existence of an exponential here. Moreover, the value …

It's well understood at this point that China's results are simply not purely the result of distillation. They're the result of significant investment with a willingness not to mak…

You can disagree, but simply stating disagreement isn't substantive. Linux can be enormously important while also not being subject to exponential value creation through improvemen…

Linux is not a relevant comparison, because the fundamental capabilities of an OS do not grow exponentially with time or investment. If building full sovereign ownership of the pro…

The keyword in your sentence is "access". The rest of the world would have cheap access to AI, but no ownership of anything at the frontier. If the US joined the rest of the world,…

You're not seeing it because you're thinking in terms of internal US economics, but this is a question about international economics and geopolitical leverage in the distant future…

Perfect -- that's great to see. The proof strategy in Lean appears essentially identical to the natural language strategy (as much as is reasonably possible). I think this settles …