20
Stubsack: weekly thread for sneers not worth an entire post, week ending 2nd August 2026 (awful.systems)
submitted 1 week ago by BlueMonday1984@awful.systems to c/techtakes@awful.systems
170 comments fedilink hide all child comments

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 - both for starting this, and for covering the previous week. We should get a bot to automate this...)

you are viewing a single comment's thread
view the rest of the comments
[-] rook@awful.systems 10 points 6 days ago* (last edited 6 days ago)

As an interesting follow-up to the ai-does-maths-using lean4 stubstack comments on Sunday, an llm accidentally uncovers a bug in the lean4 kernel.

Summary by Meven Lennon-Bertrand:

https://lipn.info/@mevenlennonbertrand/116997917683191056

To summarize:

  • an AI agent let loose provides a sorry-free proof of the Collatz conjecture
  • the proof is detected as actually being a kernel bug
  • the bug is related to (nested) inductive types, for which there is no clear theoretical specification: the kernel's code is the reference
  • external checkers (lean4lean and nanoda from a week ago) reproduce the bug, because they essentially copied the reference kernel implementation

Eta: “sorry-free” in this case means a complete proof with no trust-me-bro steps or TODOs… the sorry tactic in lean “proves” a theorem to be correct even if it is garbage or incomplete. More programming languages should make developers apologise for half-arsing their work.

And so

  • AI raises the bar for kernel correctness by a lot
  • without a clear type-theoretic understanding of what is actually implemented, we're toast
  • external checkers help to catch implementation bugs, but without a clear specification they can't catch logic bugs

How bad this is, is unclear just yet… probably not the sky actually falling, but not great. Interesting though.

[-] rook@awful.systems 5 points 5 days ago* (last edited 5 days ago)

A little bit of plot thickening spotted by abadidea: https://infosec.exchange/@0xabad1dea/117002106099986943

tl;dr, the timeline looks like this:

  • “proof” of collatz conjecture released
  • bugs identified in lean kernel
  • proof demonstrated to use these bugs

There was only a day between the first two events, and the non-proof was not where the bugs were discovered. So maybe it was just a coincidence that the chatbot found the bug at the same time, or maybe it’s training data included previous investigations into those bugs which it then built upon and that would be a bad thing for other llm generated proofs.

The collatz conjecture is sufficiently famous that enough third-party checking was done to spot the problem. I wonder how much checking would have been done on proofs of less famous and interesting things.

[-] rook@awful.systems 5 points 4 days ago

And a follow-up by talia ringer, who observes that there have always been gaps between the type-theoretic underpinnings of things like the lean prover and their actual implementation, and this hasn’t been so much of an issue til now because theorem provers haven’t had the attention of people in high places, and the type-theoreticians have been able to catch up in due course.

https://mathstodon.xyz/@TaliaRinger/117005740997367321

My big worry right now is that if organizations continue to fund the crap out of Al for formal proof research (and to generally support implementation and maintenance of proof assistants like Lean as part of that effort) but don't bother funding the type theory side of things, those gaps will grow larger and will be exploited more often by Al tools via reward hacking. Whereas people tend to only exploit kernel bugs to make a point that the bug exists. Thus proof assistants will grow less trustworthy over time.

Anyone want to place any bets on whether or nor the big llm companies are going to fund academic research that isn’t obviously mechanisable right now and won’t yield any clickbait headlines?

[-] corbin@awful.systems 4 points 4 days ago

See also a question asked today on Math Overflow, "Are we stuck with Lean?". The proposed alternative, Metamath, isn't type-theoretic and thus skips the entire dialogue between type theory and proof assistants.

[-] corbin@awful.systems 8 points 6 days ago

Lean was already known to be untrustworthy and bad, although people refuse to internalize the situation because they're caught up in Buzzard's hype machine. This is extremely funny but I don't see any signs of people waking up and realizing that Lean sucks.

this post was submitted on 26 Jul 2026
20 points (100.0% liked)

TechTakes

2632 readers
78 users here now

Big brain tech dude got yet another clueless take over at HackerNews etc? Here's the place to vent. Orange site, VC foolishness, all welcome.

This is not debate club. Unless it’s amusing debate.

For actually-good tech, you want our NotAwfulTech community

founded 3 years ago
MODERATORS
dgerard@awful.systems