My main skepticism here is whether the theorems have been properly replicated in the proof. Verifying that the proof really captured the mathematical statement seems like a manual, human process, and quite hard to repeat reliably across proofs.

At least for the main accomplishment, the Tietze extension theorem, the natural language statement and the Megalodon theorem looked quite easy to correspond, and the dependency chain seemed fairly easy as well. (the fact that the proof is 10k lines is irrelevant, this is just about the theorem statement itself)

This project did not deal with some cutting-edge, esoteric or puzzle-type maths for which the formalization can be tricky - just well-trodden topology.

This is correct, with the proviso that the meaning of the claim/statement depends on the definitions and checking these can be a bit tedious. But still feasible, and better by orders of magnitude than "checking" the proofs. Abuses of notation and just plain sloppiness are a big issue though if you wish to auto-translate an informal development into correct definitions and statements for formalization.

Yeah I learning about LPCAMM2 memory was far more interesting than the repairability score.

Can we stop it with "and the results are terrifying", "and you won't believe what I found", "the <x> situation is insane", etc.? The over-hyping of low quality, low effort content is making it hard to find actually interesting or informative things.

Yea I was thinking the same thing.

When you reach for the most exaggerated, over-the-top word possible when describing something relatively mundane, what will you use when you talk about something that actually is "terrifying?"

“The most terrifying thing you’ve ever heard”. You can even stick with that one as long as your subjects are monotonically scary.

Find a better and more accessible solution than clickbait.

Please, do it.

"Privacy concerns found in audit of popular dev tools" (or something along those lines) would work without feeling sensationalized.

In this case I'd say the "clickbait" is justified... these results are downright horrific IMO.

Yes this one time. I’m speaking generally in response to the general plea.

I’m not sure what you mean. Not clickbait is the better alternative.

If that were true, it wouldn’t be such a popular problem. Right? Clearly HN is falling into the same pattern of all the other sites. Engagement hacking blah blah blah.

You have it backwards. If it weren’t true, clickbait wouldn’t be a problem.

I think you’re the one with it backwards.

You continue to view this through the self-centered eyes of the consumer. But you’re actually the product so your perspective doesn’t matter to the seller or the buyer. That’s why this problem doesn’t get fixed.

"better", "more accessible"? What the hell are you talking about? Clickbait doesn't make anything better or more accessible.

Instead, it makes it impossible to pre-select for interesting information. Instead of telling you what something is about, it tells you how you should feel about it. That's not improving accessibility.

I meant from the author’s perspective. Clickbait is too easy, which is probably why it’s so popular.

Oh completely. But my perspective is that we all should individually punish clickbait by not clicking. More broadly, we should strive to keep HN full of quality tech content rather than clickbait.

I love the AVX512 support in Zen 5 but the lack of Valgrind support for many of the AVX512 instructions frustrates me almost daily. I have to maintain a separate environment for compiling and testing because of it.

There was someone at Intel working on AVX512 support in Valgrind. She is/was based in St Petersburg. Intel shuttered their Russian operations when Putin invaded Ukraine and that project stalled.

If anyone has the time and knowledge to help with AVX512 support then it would be most welcome. Fair warning, even with the initial work already done this is still a huge project.

I ran my own XMPP server for about 15 years. Then 10(?) years ago Google's GChat migrated away from XMPP. I never had another XMPP conversation with anyone from that point on. I finally turned the XMMP daemon off off about 2 years ago to reduce my attack surface.

I should add that I have a group of friends that only chat on "C", for C in:

* SMS * Apple iMessage * Email * IRC * Facebook Messenger * Telegram * Slack * Webex Teams * Discord * Twitter (DMs) * Signal * Whatsapp * A particular PHPBB web forum

Instead of being on top of all of these, I mostly neglect all of them, and then friends complain that they haven't been able to get a hold of me for 6 months.

XMPP was my own "solution" to this problem, which nobody else used.

Often "nothing is changing" ends up being more literal than the founders realize or intend. Acquisitions by big companies tend to slow the development to a crawl as development bureaucracy takes over. When a great product is practically frozen in time it stops being great in 5-15 years as the rest of the world passes them by.

Yea, this is accurate in my experience.

Yeah I've spent way too much time reading this "guy's" posts here, Academia profile, etc. Huge waste of time. AI has managed to amplify a crank 100x. This is only going get worse.

I've seen for myself how much tunnel vision these models will get when collaborating scientifically/mathematically. When working around unfamiliar domains I have to do extensive grounding on my own. Curious to see how this changes over the next two years as the industry goes after scientific collaboration.

You should look. It’s almost more entertaining than the README.md

  theorem MilkyWay_Is_Collapsed : DeterminePhase MilkyWay = Phase.Collapsed := by
    -- ArkScalar MW ≈ 0.41 < 0.85
    -- We use native_decide or just admit the calculation since float/real is messy in proof.
    sorry -- Calculation verified by python script

Charles Schwab has something very similar. They keep unenrolling me from their paperless thing and then send me a letter every month telling me they unenrolled me because emails aren't being delivered.

But I get their emails just fine. It's their tracking that (intentionally) isn't working.

Capital One is the same. I eventually stopped caring; I know these paper mailings are costing them money. Maybe they'll get the point someday.

An issue is the number of banks now charging you back for paper services. At least one of my banks the fee is now $15/month for paper statements. That's way more than postage.

I'd almost prefer paper statements from a few of my accounts, but not enough to pay for it directly.

Maybe this is what's happening to me at Fidelity. They keep complaining about my email on custom domain but the Protonmail address works fine. I use different apps for the two because PM doesn't support IMAP, so maybe PM doesn't block the tracking pixels but the other one does.

I'm happy this is public domain. In 2023 I used the stain images as the basis for a CTF challenge (for BSidesSF). The encoded flag given to participants was https://github.com/BSidesSF/ctf-2023-release/blob/main/alien...

Unfortunately the challenge was a bit too hard and went unsolved during the competition.

It's hard to imagine a reason for it being kept... proprietary?

A lot of people want to slap licenses on things without really thinking about what the license will do (or prevent), in practice.

I like the author's note about the license: "As we do not believe in imaginary property, this package belongs to the public domain."

I think it's much more common to see a Creative Commons license on this sort of thing.

And even then, when people have good intentions they don't anyways know about edge cases. Please give things a licence in addition to placing it in public domain, because in some countries (like Australia) you can't release your rights that way.