upvote
Claude is underrated in math. The 10 problems that openai solved? They needed an internal version. Fable 5 solved 5 of those.
reply
Sounds really cool, were you able to verify the correctness of the results?
reply
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.

reply
You mean SMT, right?
reply
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
reply
deleted
reply
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.
reply
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.

reply
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.
reply
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.

reply