Hacker Newsnew | past | comments | ask | show | jobs | submit | sequin's commentslogin

Resist hypes and just use whatever you feel like. Torvalds uses a 40 year old EMACS implementation and that seems to be working for him.

I left Spotify years ago. Youtube is so much nicer in terms of content alone. But Youtube, with its insane backlog of video's not available elsewhere, is straight up a monopoly, so they too will start squeezing customers at some point. In anticipation of that I've been collecting flacs again. It's actually kind of a nice hobby.

YouTube’s commingling of playlists (and everything else) between music and videos made it completely unusable for me.

I am a YouTube Premium subscriber, but ended up subscribing to Apple Music to get a service that works the way I want, without screwing up other things I use.

YouTube has started screwing up as well. I was having a lot of issues with YouTube errors in Safari. Best I can tell it was due to uBlock Origin Lite. When I disabled content blockers on YouTube my error rate went down dramatically. If I’m paying for YouTube and shouldn’t see any ads, why does the site break itself when I have content blockers enabled? It seems the heavy handed measures to get free users to watch ads are also impacting Premium users. This feels wrong.


Same here!

I found now was a good time to build that NAS I wanted to have a long time ago, and the first thing I installed on it was a Navidrome server so I could listen to my curated music everywhere.

Hopefully we're entering the era of people ditching megacorp craps and switching to personal cloud solutions.

YouTube will be very hard to replace though.


I never used Spotify, get to use YouTube to find out about new artists, but what I get to play are plain old MP3, either bought directly as such, or taken from music albums that I still buy with some regularity, ideally directly from bands after attending their concert, if they happen to sell some afterwards.

I tried YouTube for music a year ago or so, as it was included when I tried out a paid YouTube plan to remove the ads. Apparently (at least at that point) not all videos are available in "YouTube Music", so you can't just play back any of the videos from YouTube while using YouTube Music via Carplay, instead you need to then use YouTube itself, which of course you can't use via Carplay.

After being disappointed again and again, I too moved back to collecting local files for my music instead, although bought rather than what.cd as I used in my early days. Tend to use Bandcamp mostly, they also waive their fee on purchases every first Friday of the month (https://isitbandcampfriday.com/), so collecting a bunch of things to buy and listen to each first friday of month has become a nice little ritual :)


Same, except moved to Qobuz. They have both streaming and you can buy downloads.

I'm just so glad I'm past the phase where I'd worry about these things. It's very exhausting.


Came here to say the same. At first I couldn't even relate, but then another phase of my life came flashing back to me. All the angst around the pretense, wondering why I like somethings in a particular space but then not others that I was supposed to like...

And then slowly over time the realization that most people were in the same boat and it's just virtue signaling

Now I like what I like, I don't like what I don't like


I doubt talking heads on the TV can move markets.


How can the models be impressive if they switch to Chinese mid-sentence? I've observed those bizarre bugs too. Even GPT-3 didn't have those. Maybe GPT-2 did. It's actually impressive that they managed to botch it so badly.

Google is great at some things, but this isn't it.


The Weezer video was quirky, funny, creative, catchy and appealing to multiple generations. A stroke of genius by Microsoft.


Probably a prank or an ambush set up by the anti-billionaires.


It is impossible for this to not be satire. Hopefully the billionaires show up, because I'm not marching shit for nothing on a Saturday.


FWIW, I just gave Deepseek the same prompt and it solved it too (much faster than the 41m of ChatGPT). I then gave both proofs to Opus and it confirmed their equivalence.

The answer is yes. Assume, for the sake of contradiction, that there exists an \(\epsilon > 0\) such that for every \(k\), there exists a choice of congruence classes \(a_1^{(k)}, \dots, a_k^{(k)}\) for which the set of integers not covered by the first \(k\) congruences has density at least \(\epsilon\).

For each \(k\), let \(F_k\) be the set of all infinite sequences of residues \((a_i)_{i=1}^\infty\) such that the uncovered set from the first \(k\) congruences has density at least \(\epsilon\). Each \(F_k\) is nonempty (by assumption) and closed in the product topology (since it depends only on the first \(k\) coordinates). Moreover, \(F_{k+1} \subseteq F_k\) because adding a congruence can only reduce the uncovered set. By the compactness of the product of finite sets, \(\bigcap_{k \ge 1} F_k\) is nonempty.

Choose an infinite sequence \((a_i) \in \bigcap_{k \ge 1} F_k\). For this sequence, let \(U_k\) be the set of integers not covered by the first \(k\) congruences, and let \(d_k\) be the density of \(U_k\). Then \(d_k \ge \epsilon\) for all \(k\). Since \(U_{k+1} \subseteq U_k\), the sets \(U_k\) are decreasing and periodic, and their intersection \(U = \bigcap_{k \ge 1} U_k\) has density \(d = \lim_{k \to \infty} d_k \ge \epsilon\). However, by hypothesis, for any choice of residues, the uncovered set has density \(0\), a contradiction.

Therefore, for every \(\epsilon > 0\), there exists a \(k\) such that for every choice of congruence classes \(a_i\), the density of integers not covered by the first \(k\) congruences is less than \(\epsilon\).

\boxed{\text{Yes}}


> I then gave both proofs to Opus and it confirmed their equivalence.

You could have just rubber-stamped it yourself, for all the mathematical rigor it holds. The devil is in the details, and the smallest problem unravels the whole proof.


How dare you question the rigor of the venerable LLM peer review process! These are some of the most esteemed LLMs we are talking about here.


It's about formalization in Lean, not peer review


"Since \(U_{k+1} \subseteq U_k\), the sets \(U_k\) are decreasing and periodic, and their intersection \(U = \bigcap_{k \ge 1} U_k\) has density \(d = \lim_{k \to \infty} d_k \ge \epsilon\)."

Is this enough? Let $U_k$ be the set of integers such that their remainder mod 6^n is greater or equal to 2^n for all 1<n<k. Density of each $U_k$ is more than 1/2 I think but not the intersection (empty) right?


Indeed. Your sets are decreasing periodic of density always greater than the product from k=1 to infinity of (1-(1/3)^k), which is about 0.56, yet their intersection is null.

This would all be a fairly trivial exercise in diagonalization if such a lemma as implied by Deepseek existed.

(Edit: The bounding I suggested may not be precise at each level, but it is asymptotically the limit of the sequence of densities, so up to some epsilon it demonstrates the desired counterexample.)


Here's kimi-k2-thinking with the reasoning block included: https://www.kimi.com/share/19bcfe2e-d9a2-81fe-8000-00002163c...


I am not familiar with the field, but any chance that the deepseek is just memorizing the existing solution? Or different.

https://news.ycombinator.com/item?id=46664976


Sure but if so wouldn't ChatGPT 5.2 Pro also "just memorizing the existing solution?"?


No it's not, you can refer to my link and subsequent discussion.


I don't see what's related there but anyway unless you have access to information from within OpenAI I don't see how you can claim what was or wasn't in the training data of ChatGPT 5.2 Pro.

On the contrary for DeepSeek you could but not for a non open model.


I am basing on Terrence Tao comment here: https://news.ycombinator.com/item?id=46665168

It says that the OpenAI proof is a different one from the published one in the literature.

Whereas whether the Deepseek proof is the same as the published one, I dont know enough of the math to judge.

That was what I meant.


Opus isn't a good choice for anything math-related; it's worse at math than the latest ChatGPT and Gemini Pro.


I find it interesting that, as someone utterly unfamiliar with ergodic theory, Dini’s theorem, etc, I find Deepseek’s proof somewhat comprehensible, whereas I do not find GPT-5.2’s proof comprehensible at all. I suspect that I’d need to delve into the terminology in the GPT proof if I tried to verify Deepseek’s, so maybe GPT’s is being more straightforward about the underlying theory it relies on?


Rather the opposite. A vibe-coded startup cannot survive if it can be trivially duplicated. The proof will be in observing the inverse phenomenon; (pure) software companies disappearing.


It's certainly morally and legally dubious to facilitate attacks on things that others choose to use in within their own private domains, just because you disagree with that choice. But that's how these people roll.


It's been 15 years since this was known broken. If you had children when it was not known broken, they'd be almost old enough to drive in most western nations.

At some point the line must be drawn.


Some are very entitled to drawing lines on someone else's property. Why don't you mind your own business?


I mean this kindly, but if you're still using net-netlmv1 on anything that matters, you need to pay much more mind to your own business because even the original vendor of it has been telling you to get off that since 1999 because it is not safe.

If you're using it on something that doesn't matter, then it also doesn't matter that rainbow tables any attacker could have already had for a decade are slightly more available.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: