rook

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.

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.