varjag

7 ms·

91.
by varjag 3mo ago
I didn't say they have no value. Just limited value. A novel readable proof that expands the horizons of human insight is certainly more valuable than a megabyte sized trychnobezoar of machine generated predicates.
92.
by varjag 3mo ago
Yes. That makes it fat, expensive and vulnerable target. There are videos of them being blown up regularly.
93.
by varjag 3mo ago
How does it matter if it Lean verified or a human verified proof if you comprehend neither? There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward.
94.
by varjag 3mo ago
Human unreadable proofs have only limited value.
95.
by varjag 3mo ago
It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.
96.
by varjag 3mo ago
Jamming broadband is a lot more energy expense than frequency hopping. Orders of magnitude.
97.
by varjag 3mo ago
You could try solving that in Lean perhaps
98.
by varjag 3mo ago
…and thank God it's not Lean.
99.
by varjag 3mo ago
What happens in countries with no rule of law is rule of power hierarchies. A regional party boss would have his trusted deputes running things, who have their underlings, they underlings have their preferred business partners (police chief
100.
by varjag 3mo ago
What did you use for the simulation part?
101.
by varjag 3mo ago
I have in fact masters in SE and three decades experience of commercial programming. Loved every minute of it (well except the burnout episode) and still do my hobby projects. So I would say no, you are wrong. The models decimate not just t
102.
by varjag 3mo ago
It's fine for your pet projects. But for most of professional programming it's no longer feasible as you'll be at a small fraction of your machine assisted performance.
103.
by varjag 3mo ago
It's not anywhere close. Like, by four orders of magnitude.
104.
by varjag 3mo ago
You know how I read new papers back in 1994? By going to the library, finding one in bi-annual publication list and requesting it through the University system. And it better be necessary because the uni had to pay both the catalogue and e
105.
by varjag 3mo ago
Engineering is used fairly loosely these days but I insist engineering ends where you have to prove theorems.
106.
The fall of the theorem economy(davidbessis.substack.com)
285 points by varjag 3mo ago|122 comments
107.
by varjag 3mo ago
Normally export controls once introduced last years to decades.
108.
by varjag 3mo ago
So two and a half weeks, and on the workday. I wonder how much Jared had made. https://news.ycombinator.com/item?id=48519513
109.
by varjag 4mo ago
Naturally I wasn't implying they'll restrict the current models retroactively. Which either way trail behind even the universally available frontier models. What's perplexing is people see CCP as some kind of libertarians whi
110.
by varjag 4mo ago
Not sure why people here are so upbeat about China. It is almost guaranteed it will also introduce export controls on the models.
111.
by varjag 4mo ago
He stopped at the point where Putin had already fled Moscow, and only because of the hostage situation with his family. I'm not sure to which degree that would have deterred Elon.
112.
by varjag 4mo ago
If you reduce a class to <10k people in the world the word loses its meaning.
113.
by varjag 4mo ago
When people hear 'underclass' there's that mental image of food stamps and homeless shelters. I suspect though the society will converge to something similar to current status quo. We'll end up having our usual comforts,
114.
by varjag 4mo ago
Seriously. At that point it was a stuff of science fiction with the early models being on level of Markov chains. Today they are more helpful that the computer in Start Trek.
115.
by varjag 4mo ago
I mean just as an exercise. Also, emojis (as well as hieroglyphics ) are still text.
116.
by varjag 4mo ago
I can assure that mobile devices and embedded systems are programmed with text and keyboards as well. As a small challenge you could try expressing the contents of your comment using visuals only.
117.
by varjag 4mo ago
You have a point but the way I see it they can't be an insignificant minority. That this is a proudly pursued official policy has one corollary: there are no perceived electoral consequences to the vice president, senators and represen
118.
by varjag 4mo ago
We have a major continental war raging on for years here with combined casualties of well over a million people. Which you're adamant is none of your business. So no, I don't think so.
119.
by varjag 4mo ago
[flagged]
120.
by varjag 4mo ago
I unironically think the solution is vibecoding your own Javascript blobs that use no frameworks and have no (or minimal) external dependencies. At this point it is entirely feasible for many kinds of projects.

More ›