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.

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.

I reprompted it, it failed again, and I ran out of tokens. I’m sure someone will tell me to shell out $200/mo for a pro subscription.

One of the things that’s never clear from the reporting on ai successes is exactly how much actual paid human time went in to achieving those successes. This was especially notable in the fable-based security work… a huge amount of person-hours went into turning fable-detections into actual meaningful vuln reports.

A lot of demonstrably clever and capable people are involved with the llms-for-maths work, and a lot of money was spent on their time and supporting their work. Replicating it without your own stable of mathematicians and computer scientists and all the tokens they can eat is probably impractical.

I believe the main ingredient is Lean, which is a formal language resembling a programming language. Math proofs written in Lean can be verified deterministically with a computer, which really helps mitigate the hallucination problems of LLMs.

Fwiw, lean is a general purpose programming language, though despite microsoft’s efforts no-one uses it for that. I think its popularity with mathematicians came as a bit of a surprise.

Anyway, the other important thing that didn’t get reported on is that building the formal definition of the problem is not trivial! Obviously I don’t need to tell you that, but from the reporting you’d think that an llm solved all these problems, when in fact it was an llm in the hands of some very capable people who absolutely did not just prompt the thing in plain english.

Anyone hoping for self-marking homework here is going to be disappointed… lean slop confirming to formal spec slop is just expensive slop. Reviewing regular genai code is awful, even the thought of reviewing genai dependently-typed code makes me want a new career.

Multi-trillion-dollar (-self-valued) industry that’s the future of all work and that everyone who doesn’t use it gets left behind and everyone who does use it evokes superheroically productive turns out to be helpless in the face of a small group of outspoken and minimally organised opponents?

I see.

Humanoid robots providing stiff competition to quantum as to where the smart desparate money will be going once everyone realises the wheels have fallen off ai.

https://thepit.social/@peter/116962244994361810

(the video is too big to upload here)

I particularly like the way they had body bag operatives within lunging distance, because they clearly expected the thing to just fucking die at a moment’s notice.

Or maybe they do that for all their speakers.

This is funny yet also awful: adversarial tokenmaxxing suggests that writing everything as l33t$p34k increases the cost to process a document with an llm because the initial tokenisation step produces far more tokens.

This seems like it shouldn’t be too hard to work around, if it became commonplace (which it won’t) but the prospect of any anti-llm places doing this in the meantime does not spark joy.

I’m deeply suspicious of this whole thing, because it looks a lot like a marketing exercise showing off how dangerous and powerful and autonomous their product is.

Also, “sandbox” is one of those words that the llm companies have ruined, because they use it to mean a strongly-worded sentence telling an llm not to do something.

The author tends to cull his own social media posts pretty aggressively if they get too much attention, or the wrong kind of attention, and it’s possible there’s more he wanted to say in the blog post but he chickened out at the last minute and self-censored it.

But yeah, it felt like half a post.

Tales from Earthsea is also good.

I didn’t mind The Other Wind… it isn’t as good as the others, but that’s a tough act to follow. It does draw together a bunch of plot threads from the previous books and provides a kind of closure, which I appreciated. There was more to say of Earthsea, but le Guin wasn’t going to have the time or energy for that.

Nah, this isn’t the endpoint… you want something like prompt2exe, which is a performance art piece. Gets an llm to output machine code, and bundles it into an executable.

no package dependencies and invokes no assembler, compiler, or system linker.

Hardcore mode. No handholding for puny human devs by their tool chains. 🦾

Probably impractical for normal people to run, unless they have an employer who wants their minions to be burning all the tokens and pays up for the expensive kind of accounts.

Daft ai project of the week: “lore”, a version control system that should not be confused with another vcs of the same name open-sourced by epic games a few weeks ago.

lore does not track your code. it tracks the prompts, notes and decisions that produced it. you commit intent. when you want code, you run lore materialize: it replays the accumulated intent into a brief, and an agent reconciles the working tree to match it.

the code is build output. the intent is the source.

…which would be great, if the output of llms were deterministic, and generally it is not. This means rolling back a change to undo or fix something is just another spin of the roulette wheel, with the analogy being reinforced by the number of tokens you’ll have to buy and burn to do a rebuild. It looks like it still needs a real vcs behind the scenes, given that it isn’t entirely self-hosting, but maybe I misunderstood something.

You might wonder if this is some kind of satirical work, or perhaps piece of performance art, but I’m fairly certain it isn’t… the creator and sole human author (naturally, claude is the only other “contributor”) is a big fan of something called “open audio protocol” and a project called “audius” which came about by someone asking what if spotify and soundcloud, but on the blockchain? With ai agentic integration?

https://github.com/lorevcs/lore

I can actually elaborate on my time up there if anyone is interested. Theres even a infosec angle.

I don’t understand why this is a question. Why would you not elaborate?

I have a weird urge to do those sorts of road trips, probably because I’ve seen a lot of video that only shows the most interesting bits and it’s not something I can easily do here… the northernmost roads of the uk are decidedly not very remote, and tend to be choked with campervans.

I’m more familiar with vox day than I’d really like. He hasn’t pivoted from the culture war stuff that he’s known for, but he has branched out into ai music and video these days.

More ai stuff, this time from flathub: Democratizing Abandonware.

Flathub has a fairly relaxed ai policy that both ai bros and strongly anti ai people are unhappy with. It was brought in to try and deal with the review burden of slop submissions where no human is involved, and a chatbot fields review comments.

Turns out that ~75% of submissions that got a slop tag were abandoned… not just the submission, but the entire git repo behind it, too. The author is quick to point out that this is far from a representative study, but I can certainly believe that a) people who have invested little time or effort into their slopware will abandon it without much concern, and b) things like openclaw could definitely submit bullshit packages that are immediately forgotten as its internal state moves on. There’s no malice in the same way there’s no intent, just shitty tools being left running and polluting everything around them.

what they can do is mitigate the effects of those data centers

Oooor, and I know this is a bit of a wild idea, they could instead not offer llm search.

I’m hoping my own qualifications sufficiently predate the llm era that I’d be safe from that particular filter, so I’ll only have to worry about being too old and/or too expensive.

Whilst I try and remember, there’s this older post by blackle mori , a joke about doing undercover data harvesting work for llm companies by pretending to be a teacher and scanning children’s schoolwork.

Which was then followed in the real world by Researchers Wanted Preschool Teachers to Wear Cameras to Train AI (paywall) because satire is impossible now, I guess? I can’t find out if the plan ever came to anything, though.

A couple of bits of nice ai news recently, for anyone who hasn’t come across them already:

Bosses Horrified as “AI Native” College Graduates Hit the Workplace

new hires who were seen as “AI natives” are turning out to have alarmingly shallow ideas. So much so, the anonymous finance worker admitted, that his firm now actively avoids seeking out AI-literate STEM graduates, and opts to comb through humanities students instead.

“We want critical thinking, not just AI,” the financier told the FT.

I can’t help thinking that, funny as this is, the people who are really going to the be worst off here are a bunch of new grads with a load of debt and an education that has made them less able to do anything at all. They’re not all going to be grifters, after all.

Meta’s Zuckerberg says AI agent tech progressing slower than expected

This is brilliant. They’re making so many mistakes they’re actually having to admit it. It’s amazing how incompetent zuckerberg is… late to every fad he’s tried in the last decade and fucks it up when he finally gets there.

In retrospect, he said, the “trajectory of the agentic development over at least the last four months hasn’t really accelerated in the way that we expected,” and ​that the company’s bets on the new structure “haven’t come to fruition yet.” Zuckerberg was referring to AI agents, automated systems that can ​execute tasks on behalf of a user.

Conversations he was having “with our top people” when they started planning the restructuring in January and February “were that they ‌were ⁠worried that we weren’t going to move fast enough to adapt,” Zuckerberg said.

I’m sure there was a third thing, but I found it yesterday when the site appeared to be down (at least for me) and now I can’t remember it or spot it in my million open tabs.

Here’s one from the archives: https://spectrum.ieee.org/children-beating-up-robot

Children Beating Up Robot Inspires New Escape Maneuver System

tl;dr: small children have no empathy for your robot and will torture it and hound it to death if they can. The safest thing to do is to head for the nearest adult-sized people, who will hopefully be less inclined to kill it simply because it is a robot.

I wouldn’t want to do that myself… personally too much tracking gear in there, and it’s easy to make a mistake and not disable it all. Also, you just know that if you get caught, they’ll try and prosecute it like you kidnapped and dismembered a regular officer.

Now, I’m more surprised that they don’t get black bagged and tipped over. Maybe they only ever use them in super thoroughly surveilled areas with nearby human backup, but you’d expect at least one successful tipping to make the news somewhere.