I’ve seen a suggestion that it was a deliberately provocative marketing stunt to pump sales a little and keep the ellison estate healthy, and I kinda hope so but too many people are getting the brain worms for this to be a safe assumption 🫤

New book: superlawyers! how claude makes you the best lawyer in the room.

https://www.amazon.com/dp/B0GHYS5FC2

The author even shares his prompts for free!

https://github.com/danlorry/superlawyers-prompts

Every prompt here is designed for that pattern: Claude multiplies your judgment, never replaces it. The prompts are ready to paste into Claude. The book explains why they are structured the way they are.

The prompts mostly seem to be structured as “imagine you are an attorney. Now do this homework exercise”. There’s a passingly interesting idea around having the chatbot attempt to form a counter argument to your own claims, which you can then use to make your own position stronger, which seems like it might actually be a genuinely okay idea especially if you expect your opponents to be llm sock puppets, but everything else looks pretty much like garden variety “do my thinking for me”.

I’ll admit I didn’t read the prompts closely, so may be I’m being uncharitable, but I doubt there are many nuggets of gold hidden in there.

h/t to rahaeli

Grokipedia hasn’t been updated for months: is it because

• it has been vibe coded into unmaintainability
• the people responsible for it no longer care
• the people responsible for it are utterly incompetent
• all of the above?

I’m assuming that it isn’t “the llm bills were too high” just yet, but maybe it could be that, too.

https://futurism.com/future-society/grokipedia-broken-nobody-noticed

Posting scurrilous and unverifiable gossip.

Sam Altman matched with a man on Grindr, who posted the conversation. Open AI offered him money to take it down.

He made a song instead.

https://bsky.app/profile/valarmordollars.bsky.social/post/3msgqy34gvc2d

Personal highlight for me was the chat screenshot:

Altman: “I’m lonely and horny” Frostedjake: “as u should be”

💀

May working in the ai sector do for your lovelife what being openly republican does.

Nah, that’s just the global-warming-induced warm water they like, the presence of a reactor was incidental… swarms around any sort of suction system are going to be a problem.

I can offer you a upgrade in the form of an array of radioactive spinning blades if you’d like.

(in theory you could deploy your data centres in places where nutrient levels are low, so there’s less plankton and so a much reduced risk of jellyfish swarms, but I have absolutely no faith that these cowboys would even stop to think about that for one moment)

Not sure who Wes Streeting is

I’d say he is a shitty transphobic blairite labour politician and current cabinet member, but I don’t know how much that narrows things down. He holds a non-trivial amount of political power in the uk. There was a brief moment where it looked like he’d replace keir starmer.

I’ve been thinking about open source contributor policies recently, and been unhappy with what I came up with. This is so much better.

PRs welcome. No, not from you, and definitely not from them.

Ahh, but you can sterilise the incoming seawater by irradiating it, and by a happy coincidence I’ve come up with a way to reduce the cost and weight of the reactor shielding.

Well, you know how everyone went from “do not trust anything you read on wikipedia” to “wikipedia is the last hope for humanity’s knowledge and history”?

So this one seems to be somewhat up in the air right now, and could do with a bit more verification, but it appears that google might be training gemini on your private google docs and a gemini user could ask questions that expose the contents of those documents.

Which is interesting. We use google docs at work, but it isn’t clear how much valuable ip or confidential information is in there.

https://www.reddit.com/r/IndieDev/comments/1vfwuf5/a_player_found_out_the_actual_name_of_my_games/

Amazing installation instructions at https://github.com/0xeb/ghidrasql

Install with an AI agent (recommended)

The fastest way to get ghidrasql running end-to-end is to point an AI coding agent (Claude Code, Cursor, Codex, Aider, etc.) at the bundled installer prompt:

install-prompt.md

It is a self-contained runbook with explicit verification gates at every step — preflight checks, building libghidra, installing the LibGhidraHost Ghidra extension, building ghidrasql, and a first live query. Hand it to your agent and let it drive the install; intervene only if a gate reports a failure.

JFC.

h/t to rairii: https://labyrinth.zone/objects/96478395-64d9-452c-a906-9e6159cd10a3

I was gonna link someone else’s observations on it, but got sidetracked by a shiny object or something.

https://mastodon.catgirl.cloud/@49016/117021988214007605

They didn’t link the sources, but apparently the all-my-apes-gone twitter crowd are still breathtakingly ignorant of technology and statistics, despite how many years of bitcoin catastrophes have passed.

Quite a few people suggesting/using dice to mitigate the Coldcard vulnerability.

Note that common dice are not designed to be cryptographically secure.

If you are going to do this, you probably should buy precision casino dice. And even then, have another source of entropy.

Posted entirely unironically, apparently. Hard to say, but Poe’s law has yet t be repealed.

As comedy art projects go, I really admire their dedication to the bit. The images are remarkably high quality, and they’ve really thought long and hard about those designs. I mean look at this… it’s glorious.

I’d advise against attempting to disable a chainsaw operator by poking them with a knife, though. I guess it’s too bad that pitchforks are pretty uncommon these days.

he didn’t hedge on long enough timelines

Duh. Everybody knows the market never stays irrational for long, and you should just tough it out.

Salt water is famously a forgiving environment to build in, and oceanic weather is benign and predictable. Not that it would be a problem anyway, because move-fast-and-break-things people can be trusted to do the right thing when it comes to running delicate equipment in places more hostile than mid california, and will not skimp on staffing and maintenance. You can look at all the the successful seasteading operations to see how well this will go.

There are also no problems I can foresee with putting a bucketload of fissiles in international waters, with no scope for finally uniting old-school piracy with new-school piracy, either. This plan is great, and no-one will have a problem with it.

It sounds like a contract killing operation run by openai.

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?

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.

To be extra grumpy… seems to me that most note-taking apps have always been a bit shit, and coding assistants have just pushed them over the edge. All vast electron apps with terrible sandboxing as far as the eye can see.

I quite like the linked-text-document model for various things, and it would be nice if someone could make an editor that a) didn’t use electron and b) could do something like html export. Oh, and c) supported plugins that don’t get unrestricted access to my entire filesystem.

Not even any closed-source options manage that, though. Everything is just bloat and security vulnerabilities as far as the eye can see.

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.