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.

So none of this suprises me.

▲

bauldursdev 14 hours ago | parent | next [-]

Sounds really cool, were you able to verify the correctness of the results?

▲

MWil 14 hours ago | parent [-]

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.

▲

rsrsrs86 12 hours ago | parent | next [-]

You mean SMT, right?

	▲	MWil 9 hours ago \| parent [-]
		my memory was that SMT was part of a more advanced SAT solver, as in if you want to be modern/use SOTA, your SAT solver is going to use SMT

▲

11 hours ago | parent | prev [-]

[deleted]

▲

DroneBetter 13 hours ago | parent | prev [-]

it would be useful to create an account and document your work in a post at https://conwaylife.com/forums, if you're not planning to make a blog post.

▲

MWil 13 hours ago | parent [-]

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.

▲

empath75 13 hours ago | parent [-]

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.

	▲	MWil 13 hours ago \| parent [-]
		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.