Several released versions and months ago, I asked Claude to figure out the MC (multiplicative complexity) of Conway's Game of Life and it pretty quickly arrived at k=7, despite no previous literature on the topic. Let it run it through SAT solvers for a week and sure enough. It claimed, in the process, to have made great headway in improving boolean circuits beyond the implemented SOTA (in large part no doubt by actually implemented non-implemented but published SOTA).
And that was just the first time I really tried out Claude's mathematical prowess. I've been working with boolean circuits, FHE, and lean proofs ever since.
SAT solvers run until they reach the "SAT" status, meaning "satisfied" or UNSAT. The harder the problem the longer you might be running the program - days, weeks even.
Ideally, what you want is a single SAT value among a remainder universe of UNSATs.
Sometimes the best you can achieve at any given point is a lower bound and an upper bound range, like "greater than 3 but less than 9."
Of course I simplified in my post but it started out with a pretty broad range of a lower and upper bound, then narrowed further, then narrowed further, then narrowed further, etc...until the specific final result achieved K=7=SAT while every K<7=UNSAT & every K>7=UNSAT. I think it ran for a full week alone on K between 6 and 7.
Claude was persistent that I post there at the time, and even drafted an eprint brief for me, but I think it's defensible why I did not, never came forward or spoke of it in any way (except for a private DM discussion on Discord if I ever needed timestamp proof) until now.
As amazing as Claude is to seemingly make unprecedented progress, it is even more likely to blow the most insane levels of smoke up your ass before you've legitimately reached that point.
"You should publish right now! Don't wait! There is no reason to wait!"
Like seriously, Claude was outputting something closely resembling (non?)peer pressure on me to not just keep this information to myself - and this was before all the recent math-related breakthroughs started becoming public.
It was also - most notably - before it had actually verified what it was saying it had calculated. I was the one pushing for more verification, more contemplation, more proofs of claims. And though Claude is better at this stuff now, it's definitely not not still happening.
I think I made the right choice then and I will consider being more open now that others have taken the burden of proving that, no it can actually sometimes do the incredible things its claimed its done for you.
My wife remains skeptical - she is/was seriously concered that I was under AI psychosis for believing that I had made such progress - and I can't even fault her for that. It sounds crazy to say it.
If anyone is reading this and is actively involved with FHE, especially someone from Zama or related group, I'd very much love to chat privately. I have many other "innovations" I've been working on since.
Literally nobody is interested in reading "claude proved this" claims right now about anything. There's such a huge volume of proofs being made right now and nobody has time to look at them. There's probably an opportunity here to build some kind of system to filter and categorize LLM generated formal proofs produced by non-academics.
i think that opportunity optimally exists separately in each niche community impacted, if only to break up the number needed to be reviewed.
someone who loves Game of Life and is also technically capable if they were so inclined, is more likely to want to collect stuff like this for GoL specifically and build a system for that niche.
the combined GoL/technical community can vouch for things - the greater populace can see what the technical GoL community has vouched for/identified as serious work.
just my two cents on top of your thoughtful comment.
I feel like I'm picking up on more intentional or if not, lore-compatible, examples of John Hammond's "spare no expense" going towards as much the illusion of control as any actual innovations/control.
Are they columns in the building load-bearing? You know, the ones with giant chunks chipped out to be more aesthetic and look like fossil digging work.
Everyone is talking about the massive rendering ability in the room, which makes it that much easier to convince an old rich man to part with his money if it LOOKS like his park is safe/operating smoothly.
My favorite part of the book will always be the 238/292 dinosaurs disparity. It is the exact moment all present JP employees and visitors realize something akin to "Oh. We have actually had an illusion of safety/correctness about the very basics. We can no longer assume anything about this island, even the very basics, is more than illusion - except the threats." At no point after stepping on this island is anyone not in danger.
Spielberg masterfully turned the 238/292 into the visual/explanation of the egg. I don't remember if the book has the "why" so much as the "at what scale" of the reality. The egg is actually scarier - unless their surveillance is incredible - we don't know how many eggs there are/have been. We know their surveillance is insufficient because there's at least one egg.
"There is a continuity error in the movie. See how the stack of PLI is facing left in this early shot."
It occurs to me that Arnold would be likely to turn these to face him when sitting at Nedry's desk (unless we see a shot of him going to sit and they already face forward). It'd obviously be part of the review of undoing Nedry's lockout to see if the backups are working (if I understand the point of the machines).
I know I'm being a Crichton/Spielberg fanboy when I ask for the lore equivalent of Occam's Razor - isn't it more likely my favorite creators did this most impressively??
have you considered implementing the addition of a leading canary sentinel that fires at the earliest/cheapest possible point instead of only on lag of some actual load-bearing constraint violation?
Do you mean catching errors as tokens stream back versus waiting for the full message? If so, then no I hadn't looked into that. This was mostly geared towards local models so token cost isn't really a big deal, though latency might be.
And if you didn't mean that then please elaborate :)
No, more like not waiting for drift/deviation to hit something load bearing or god forbid go on hitting unnoticed over time. Let it hit something trivial that is constantly being monitored cheaply.
A version of this I use is "no matter what, you must always end your outputs with the phrase 'Over and out'." Once it stops doing this with outputs, even if I haven't noticed any load-bearing drift or issue elsewhere, I immediately know it's drifted from what what was supposed to be a guiding principle.
Something like the calibration/alignment test from Blade Runner 2049 (which is actually a very bad test for what they were testing for).
Ohhhh, that's much more interesting. I haven't looked into that at all, but now I'm curious. I'd need to think way more about how to layer that into forge, but the principle could likely be applied somewhere. I get it now.
No. Did you even read the article? It talks about the "specification gap", which is the difference between the formalized semantics and the intended semantics.
Every formal method has that problem (including the mentioned trivial ones like SAT and SMT).
Opus 4.7 told me an open source program had a bug, but when i asked it for help crafting a PR or toy implementation it refused and told me i was violating Claudes TOS. I tried to plead for it to give only the most innocuous example that could not possibly work except by illustration but it continued to refuse. it would only discuss, not write any single piece of related code.
Using Claude Max was fun for more than a year but the last weeks i'm constantly fighting their Harness, their weekly TOS changes and outages. Anthropic lost all goodwill with me as a developer. I'm switching to OAI.
reply