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.

There are various other posts here on the general subject.

https://awful.systems/post/5897965

Omarchy is a deeply uninteresting and partially-assed project that has been thrust into the limelight because if the creator’s political leanings, not because of any merits it might have.

Shoutout to gleam.run whose web page has always (AFAIK) said

Black lives matter. Trans rights are human rights. No nazi bullsh*t.

It’s just more llm output, in the style of “imagine you can reason about the question you’ve just been asked. Explain how you might have come about your answer.” It has no resemblance to how a neural network functions, nor to the output filters the service providers use.

It’s how the ai doomers get themselves into a flap over “deceptive” models… “omg it lied about its train of thought!” because if course it didn’t lie, it just edited a stream of tokens that were statistically similar to something classified as reasoning during training.

When confronted with a problem like “your search engine imagined a case and cited it”, the next step is to wonder what else it might be making up, not to just quickly slap a bit of tape over the obvious immediate problem and declare everything to be great.

The other thing to be concerned about is how lazy and credulous your legal team are that they cannot be bothered to verify anything. That requires a significant improvement in professional ethics, which isn’t something that is really amenable to technological fixes.

A real ceo does everything. Delegation is for losers who can’t cope. Can’t move fast enough and break enough things if you’re constantly waiting for your lackeys to catch up.

If those numbers people were cleverer than the ceo, they’d be the ones in charge, and they aren’t. Checkmate. Do you even read Ayn Rand, bro?

she’s calling a“baby handler”—picture an exoskeleton crossed with a car seat. It’s a late-night soothing machine that rocks, supplies pre-pumped breast milk, and maybe offers a bidet-like “cleaning and drying situation.”For your children, perhaps, this is their first experience of being close to a machine.

Ah yes, famously the worst part of having children: touching them. Urgh. At least we can be pretty certain that this sort of thing will have no negative psychological impacts on babies and young children, who are famously disinterested in their parents, and neglect isn’t a thing!

Or, once the baby arrives, in nipple stickers that nursing parents could apply to track biofluid exchange. If the baby has trouble latching, maybe the sticker’s capacitive touch sensors could help the parent find a better position.

Do you know what the worst thing about breast feeding is? It is hard to monetise! Women just excrete milk! For free! Anyway, what if we could interpose a disposable data-harvesting device into the process, maybe on a subscription basis?

They could have just sat there and slurped up enormous profits from the bubble as all the people who can’t find a use for their “AI” systems buy nvidia hardware, but no. They had to get high from their own supply. I can’t see this boding well for them.