Stubsack: weekly thread for sneers not worth an entire post, week ending 4th October 2026 - awful.systems
awful.systems
(The spooks shall soon be upon us.) Have a sneer percolating in your system but not enough time/energy to make a whole post about it? Go forth and be mid - welcome to the Stubsack, your first port of call for learning fresh Awful youā€™ll near-instantly regret. Any awful.systems sub may be subsneered in this subthread, techtakes or no. If your sneer seems higher quality than you thought, feel free to cutā€™nā€™paste it into its own post ā€” thereā€™s no quota for posting and the bar really isnā€™t that high. > The post Xitter web has spawned so many ā€œesotericā€ right wing freaks, but thereā€™s no appropriate sneer-space for them. Iā€™m talking redscare-ish, reality challenged ā€œculture criticsā€ who write about everything but understand nothing. Iā€™m talking about reply-guys who make the same 6 tweets about the same 3 subjects. Theyā€™re inescapable at this point, yet I donā€™t see them mocked (as much as they should be) > > Like, there was one dude a while back who insisted that women couldnā€™t be surgeons because they didnā€™t believe in the moon or in stars? I think each and every one of these guys is uniquely fucked up and if I canā€™t escape them, I would love to sneer at them. (Credit and/or blame to David Gerard for starting this.)

Want to wade into the sandy, spooky surf of the abyss? Have a sneer percolating in your system but not enough time/energy to make a whole post about it? Go forth and be mid: Welcome to the Stubsack, your first port of call for learning fresh Awful youā€™ll near-instantly regret.

Any awful.systems sub may be subsneered in this subthread, techtakes or no.

If your sneer seems higher quality than you thought, feel free to cutā€™nā€™paste it into its own post ā€” thereā€™s no quota for posting and the bar really isnā€™t that high.

The post Xitter web has spawned soo many ā€œesotericā€ right wing freaks, but thereā€™s no appropriate sneer-space for them. Iā€™m talking redscare-ish, reality challenged ā€œculture criticsā€ who write about everything but understand nothing. Iā€™m talking about reply-guys who make the same 6 tweets about the same 3 subjects. Theyā€™re inescapable at this point, yet I donā€™t see them mocked (as much as they should be)

Like, there was one dude a while back who insisted that women couldnā€™t be surgeons because they didnā€™t believe in the moon or in stars? I think each and every one of these guys is uniquely fucked up and if I canā€™t escape them, I would love to sneer at them.

(Credit and/or blame to David Gerard for starting this. The spooks are well underway.)

  • scruiser@awful.systemsEnglish
    7Ā·
    13 days ago

    You know how AI proofs are supposed to be credible because of formalization with Lean?

    There is another problemā€¦ apparently Lean4 hasnā€™t actually been fully formally verified. And in fact could have more bugs lurking in it, maybe even some foundational problemsā€¦ Lesswrong post explaining the problems.

    OpenAI can more easily market that their AI is intended to fully replace mathematicians, and that this is only the herald of their general superintelligence (and not that math is the only thing working out for them).

    Yeah, this has been driving me crazyā€¦ reading places like hackernews or r/singularity, I keep seeing people assuming mathematicians and just bitter or engaging in sour grapes and that is why they are complaining about the ā€œproofsā€ OpenAI dumped out. Like it is just some small niggling detail that the proofs canā€™t be read by humans and that Lean may have bugs and that some of OpenAIā€™s proofs have already been shown to have critical mistakes.

    Edit: I had the thought to collect some links in one place Here are some more discussions on lean and autoformalization for anyone looking for good sources:

    Edit 2: Made a top level post: https://awful.systems/post/9997783