Yeah, I don't connect my TV to WiFi at all; as long as TVs have HDMI ports I'll just use an Nvidia Shield TV (or something similar). If I do that I have access to more apps, a snappier interface, and it's easier to upgrade if I need to later.

I've looked into flashing it to use a dumber firmware, but it got into technical documentation that I don't really understand really quickly. I haven't looked into it since I got a Claude Code membership though, so it might be worth revisiting with AI assistance.

Oh, no, before everything kind of converged to OpenGL and DirectX, there were oodles of different things trying to be the next graphics API.

There are the more obvious ones like 3DFX/Glide, but there was also stuff like the Diamond Edge 3D, which used Sega Saturn style "quads".

Wine is a project that I've grown a near-infinite level of respect for.

I don't know for sure, but I suspect that a lot of the work for Wine is boring and thankless. Digging through and trying to get exact parity with both the documented and undocumented behavior of Windows for the past 30 years doesn't sound fun, but it's finding every little weird edge case that makes Wine a viable product.

The fact that Wine runs a lot of games better than Windows now (especially older games) shows a very strong attention to detail and a high tolerance for pain. I commend them for it.

I used Cockpit for years after I started having issues with my network card in FreeNAS. It's generally very good, though I never really figured out how to graphically swap out a hard disk in a RAID without trashing the data (which happened once).

I suspect that was user error on my end, so if you want a more-or-less no-nonsense way to manager a server, it's certainly worth checking out.

It's definitely gotten considerably better, though I still have issues with it generating proofs, at least with TLAPS.

I think behind the scenes it's phoning Wolfram Alpha nowadays for a lot of the numeric and algebraic stuff. For all I know, they might even have an Isabelle instance running for some of the even-more abstract mathematics.

I agree that this is largely an early ChatGPT problem though, I just thought it was interesting in that they were "plausible" mistakes. I could totally see twelve-year-old tombert making these exact mistakes, so I thought it was interesting that a robot is making the same mistakes an amateur human makes.

I remember when ChatGPT first came out, I asked it for a proof for Fermat's Last Theorem, which it happily gave me.

It was fascinating, because it was doing a lot of understandable mistakes that 7th graders make. For example, I don't remember the surrounding context but it decided that you could break `sqrt(x^2 + y^2)` into `sqrt(x^2) + sqrt(y^2) => x + y`. It's interesting because it was one of those "ASSUME FALSE" proofs; if you can assume false, then mathematical proofs become considerably easier.

Let me just preempt this by saying that I think you and tomhow do a very good job at moderating, and I'm just some goober on the internet sitting on a high-horse, so take what I say with as much respect as possible.

Hacker News is my favorite forum in no small part because this forum's users are, on average, a lot more educated than the average internet user. If not formally, a lot of the people here still do value learning and education as a whole. Those environments aren't organic on the internet, and it is largely due to efforts from folks like you to cultivate this audience and I do not want to dismiss that.

The concern, then, is that when the educated people can't discuss (and let's be honest, argue about) politics, then the only people who will be discussing politics will be the uneducated people. Politics is inherently contentious and we can't make progress (however you want to define it) without occasionally hurting feelings.

Now, a perfectly valid counter to this is "we're not stopping you from discussing contentious political issues, you're welcome to discuss it on one of the many other forums on the internet, just not here". That's fair enough, but it can come off as a little arbitrary, because virtually anything can be deemed "political"; I could argue that disagreements with type systems or the ISO standard of C or complaining about SQLite could be construed as "politically motivated".

I do realize that a line has to be drawn, though. The last thing I want is for the forum to devolve into 8chan or The Drudge Report or something, so while I don't completely agree at where you draw the line, I do understand why it is drawn.