4 ms·

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

by MWil 2mo ago

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 2mo ago
Sounds really cool, were you able to verify the correctness of the results?
- MWil 2mo ago
  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 2mo ago
    You mean SMT, right?
    - MWil 2mo ago
      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
  - deleted 2mo ago
    [deleted]
DroneBetter 2mo ago
it would be useful to create an account and document your work in a post at https://conwaylife.com/forums https://conwaylife.com/forums, if you're not planning to make a blog post.
- MWil 2mo ago
  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 2mo ago
    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.
llelouch 2mo ago
Claude is underrated in math. The 10 problems that openai solved? They needed an internal version. Fable 5 solved 5 of those.
josteinhylin 2mo ago
[dead]

by MWil 2mo ago

bauldursdev 2mo ago

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

MWil 2mo ago
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 2mo ago
  You mean SMT, right?
  - MWil 2mo ago
    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
- deleted 2mo ago
  [deleted]

DroneBetter 2mo ago

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

MWil 2mo ago
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 2mo ago
  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.

llelouch 2mo ago

Claude is underrated in math. The 10 problems that openai solved? They needed an internal version. Fable 5 solved 5 of those.

josteinhylin 2mo ago

[dead]